[isabelle-dev] NEWS: split!

Tobias Nipkow nipkow at in.tum.de
Thu Aug 11 07:43:01 CEST 2016


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

-------------- next part --------------
A non-text attachment was scrubbed...
Name: smime.p7s
Type: application/pkcs7-signature
Size: 5135 bytes
Desc: S/MIME Cryptographic Signature
URL: <https://mailmanbroy.informatik.tu-muenchen.de/pipermail/isabelle-dev/attachments/20160811/b6a3d0ff/attachment.p7s>


More information about the isabelle-dev mailing list