Tracking potential changes of JML ref that affects KeY

[wadoon]

This issue tries to track changes for KeY that arise of the current discussion for the next JML ref version on Github.

• Add \old, \pre, and \before, and \invariant_for(obj, A) with a label: Pre-defined labels: "Here, Pre, Old"
  • Functions
  • Label
• Also \fresh(o, L) may has a label
• Explicit Naming for JML constructs, like contracts, clauses or invariants
  • Github
• Text Blocks
• Overloaded operators for locset
• no_state becomes heap_free
• Hilberts Operator with \choose