Re: [isabelle] structured induction proofs using customized induction scheme



On Fri, Feb 5, 2010 at 10:28 AM, Andreas Lochbihler
<andreas.lochbihler at kit.edu> wrote:
> the problem is with your induction rule. The two cases that do not work
> (UpdR and Obj) both meta-quantify over the variable L that does not occur in
> these two cases. When you delete the L in both cases in the rule, everything
> should work fine.

On Fri, Feb 5, 2010 at 11:50 AM, Lawrence Paulson <lp15 at cam.ac.uk> wrote:
> The two problematical subgoals contain schematic type variables. Enabling "show types" reveals them. See attachment.
> Larry Paulson

Oh, copy and paste error ...
Thank you both very much. Everything works fine now.

Regards,
Bianca.





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