Re: [isabelle] need help with quantified ints



On Fri, 20 Jun 2008, John Matthews wrote:

> I'm not sure why cases doesn't allow you to split on meta-bound 
> variables, as this would be less confusing for new users. Similarly for 
> induct vs. induct_tac.

In a proper Isar proof you can never access hidden information from the 
goal state, such as bound parameters.  The case_tac/induct_tac versions 
merely imitate the old tactical behaviour.

In your example there was no point to bind the outer parameters anyway, 
and you can start right away on the problem presented in an open form 
(fixes/assumes/shows, with fixes optionally implicit).


	Makarius






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