[isabelle-dev] NEWS: 'subgoal' command

[Makarius]

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


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.


 	Makarius