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> 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.