* 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
_______________________________________________
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
