Problem statements in KeY file can now also be a (semi-)sequent

[wadoon]

On request, this PR changes the grammar of KeY files, s.t. problem statements can also be sequents.

• Previous: problem: LBRACE term RBRACE;
• Now: problem: LBRACE termorseq RBRACE;

This means, you are allow to write

\problem {
   a,b,c 
    ==> 
     d, e, f
}

in KeY files.

[github-actions]

Thank you for your contribution.

The test artifacts are available on Artiweb.
The newest artifact is here.

[codecov]

Codecov Report

Merging #3283 (605922f) into main (f6b120c) will decrease coverage by 0.01%.
The diff coverage is 64.70%.

@@             Coverage Diff              @@
##               main    #3283      +/-   ##
============================================
- Coverage     37.76%   37.75%   -0.01%     
- Complexity    16863    16864       +1     
============================================
  Files          2052     2052              
  Lines        125687   125697      +10     
  Branches      21234    21236       +2     
============================================
- Hits          47464    47462       -2     
- Misses        72389    72398       +9     
- Partials       5834     5837       +3     

Files	Coverage Δ
...ore/src/main/java/de/uka/ilkd/key/proof/Proof.java	76.85% <100.00%> (-1.11%)	⬇️
...de/uka/ilkd/key/proof/init/KeYUserProblemFile.java	74.35% <60.00%> (ø)
...de/uka/ilkd/key/nparser/builder/ProblemFinder.java	64.00% <50.00%> (-9.69%)	⬇️

... and 1 file with indirect coverage changes

📣 We’re building smart automated test selection to slash your CI/CD build times. Learn more

[mattulbrich]

That would be a nice feature. ... Wanted to have that for a while.

[WolframPfeifer]

Nice feature, thanks!

I added a single commit where I renamed problemTerm to problem (and similar occurrences) for consistency.