* Splitter in simp, auto and friends:
- The syntax "split add" has been discontinued, use plain "split".
- For situations with many conditional or case expressions,
there is an alternative splitting strategy that can be much faster.
It is selected by writing "split!" instead of "split". It applies
safe introduction and elimination rules after each split rule.
As a result the subgoal may be split into several subgoals.

If you have long-running simp or auto calls in situations with a number of if and case expressions, split! could help. If you find it does, drop me a line, thanks.


In f8e79d14d61f.

Attachment: smime.p7s
Description: S/MIME Cryptographic Signature

isabelle-dev mailing list

Reply via email to