[isabelle] Enter MATCH



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.