Re: [isabelle] exception UnequalLengths raised (line 543 of "library.ML")



On Wed, Jul 15, 2015 at 12:16 AM, Manuel Eberl <eberlm at in.tum.de> wrote:

> The problem seems to be in Rule_Cases.extract_assumes, so Makarius is
> probably the one to answer your question if the UnequalLengths exception
> is the intended behaviour and where it comes from.
>
> However, what I can tell you is that what you are doing is not what you
> want to do anyway:
>

Thank you for the thoughtful response with tips. I should have mentioned in
my original message that I had proven it. The example was something I typed
along the way. Figuring out to swap the order was the hardest part for me.

Thanks,
Jason



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