* 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.

Tobias

In f8e79d14d61f.

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

_______________________________________________
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev

Reply via email to