Re: [isabelle] Enter MATCH



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.