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.
On 24 Jan 2014, at 18:28, John Wickerson <johnwickerson at cantab.net> wrote:
> 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?
This archive was generated by a fusion of
Pipermail (Mailman edition) and