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



Hi,
Marc Weber <marco-oweber at gmx.de> schrieb:
> --- simple.thy ----
> theory simple=HOL:
> lemma fist_theorem: "A-->(B-->A)"
> apply(rule impl)
> [... ^ error appears here ]
the name of the rule is "impI" (the last letter is an 
uppercase 'i') and not "impl". The name comes from 
"implication _I_introduction.

Achim





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