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



This is because impl is invalid -- you are intending to use impI
instead. So, this would work:

theory simple=HOL:
lemma first_theorem: "A-->(B-->A)"
apply(rule impI)
apply(rule impI)
apply assumption
done
end

Mark 

-----Original Message-----
From: cl-isabelle-users-bounces at lists.cam.ac.uk
[mailto:cl-isabelle-users-bounces at lists.cam.ac.uk] On Behalf Of Marc
Weber
Sent: Thursday, January 12, 2006 9:21 AM
To: isabelle-users at cl.cam.ac.uk
Subject: [isabelle] Can't isabelle-users at cl.cam.ac.uk

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

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

error:
** 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);
end
---------------------------------------

Marc






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