[isabelle-dev] NEWS: 'subgoal' command

Makarius makarius at sketis.net
Thu Jul 2 14:30:10 CEST 2015

* Command 'subgoal' allows to impose some structure on backward
refinements, to avoid proof scripts degenerating into long of 'apply'
sequences. Further explanations and examples are given in the isar-ref

This refers to Isabelle/441fdbfbb2d3, which also contains the 
documentation and examples.

Practical experience will show what are the full consequences.  E.g. how 
close do we get to a situation without the need for rule_tac, case_tac 
etc. with their implicit access to hidden goal paramaters.

It should also solve certain indentation problems in long apply scripts.


More information about the isabelle-dev mailing list