[isabelle-dev] NEWS: 'subgoal' command
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