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

Hi I've tried to use ProofGeneral with this little example from the ETH

--- simple.thy ----
theory simple=HOL:
lemma fist_theorem: "A-->(B-->A)"
apply(rule impl)
[... ^ error appears here ]

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

Is this problem caused by isabelle or by my configuration of ProofGeneral?
I also can't use button [Command] of the ProofGeneral interface  and
text "thm impl" to insert this command. (err: not found)

The first HOL example from the Isabell/Isar reference  documentation
works.. (the whole buffer is marked blue at the end)

-- test.thy from Isabell/Isar documentation --
theory Foo imports Main begin;
constdefs foo:: nat "foo == 1"
lemma "0 < foo" by (simp add: foo_def);


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