Re: [isabelle] Enter MATCH



Could you please elaborate on what exactly is happening here? I've been
wondering about this myself for ages. Is it some kind of issue with
higher order unification?

Cheers,
Manuel Eberl

On 01/24/2014 10:03 PM, Lawrence Paulson wrote:
> This is uncommon, but can happen especially if you have complicated universally-quantified assumptions. Try simp_all instead, and then force or blast on one subgoal at a time.
>
> Larry Paulson
>
>
> On 24 Jan 2014, at 18:28, John Wickerson <johnwickerson at cantab.net> wrote:
>
>> Hi,
>>
>> I've just stated my theorem, typed "apply(induct rule: ...)" and then typed "apply(auto)" to see what Isabelle could manage on its own. All that happened was that my output window turned a strange blue colour, Isabelle said "Enter MATCH" and proceeded to output lots of random variable names. What's going on? And more importantly, what should I do to stop this happening? 
>>
>> Thanks,
>> John
>





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