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