Higher Order Proof Scripts

[wadoon]

Intended Change

This PR generalizes the usage of proof script blocks further.

Currently, you are allowed to have one proof script block at the end of a command:

onAll { auto;}

With this PR, proof script blocks can appear as a regular argument anywhere (positional and keyworded):

integer-split 
  "<0" : { auto;  }
  "=0" : { instantiate; } 
  ">0" : { tryclose; }

This allows for various constructs, e.g.,

if "cond" { .. then ..} {.. else ..}

Plan

• Do it
• Test it

Type of pull request

• New feature (non-breaking change which adds functionality)
• There are changes to the (Java) code

Ensuring quality

• I made sure that introduced/changed code is well documented (javadoc and inline comments).

[wadoon]

The semicolon is not mandatory again.

[mattulbrich]

Nice. It looks actually cleaner with this generalisation.

Not thoroughly tested since the upcoming JML scripts will put this to the test.