Expand OSS steps when saving a proof for more deterministic Proofs

[Drodt]

Intended Change

This PR improves deterministic behavior in KeY by saving the rules applied by OSS rather than a (builtin "One Step Simplifier") node.

The expanded rule applications are printed with (ossStep) so the saved proof file at least still contains the information that OSS was used. At the moment, this information is neither used nor kept when reloading a saved proof (thus, it is lost completely after one save-load-save cycle). However, in the future we might use this information to show the OSS in the UI again.

Plan

• Store whether a rule app was the result of OSS in the node?
• A UI option for expanding OSS?

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).
• I have tested the feature as follows: Tested it on multiple proof files.

Additional information and contact(s)

Work with @WolframPfeifer

The contributions within this pull request are licensed under GPLv2 (only) for inclusion in KeY.