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
overhead.

--
 Peter


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