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).
This archive was generated by a fusion of
Pipermail (Mailman edition) and