Re: [isabelle] Using an assumption as a rule

I just want to point out that the 'subgoal' command has no overhead:

Sorry, I meant textual overhead (boilerplate), not computational


> on
> the contrary, it allows to check proofs compositionally and thus in
> parallel. The explicit proof structure is also an advantage for
> maintainability.
> In some situations, 'subgoal' cannot be used, though. One example are
> schematic goal states. Then one really needs to go back to old-style
> tactical means.
> 	Makarius

This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.