Re: [isabelle] Can't isabelle-users@cl.cam.ac.uk



On Thu, 12 Jan 2006, Marc Weber wrote:

*** Error in method "FOL.rule":
*** Unknown theorem(s) "impl"
*** At command "apply".

This looks like a problem with a sans serif font. The rule is called impI -- with capitial i at the end -- for implication-introduction.


	Makarius






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