Email Gateway (Aug 17 2022 at 13:45): Email Gateway (Aug 17 2022 at 13:45):From: Marc Weber <marco-oweber@gmx.de>
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
Email Gateway (Aug 17 2022 at 13:45):From: Makarius <makarius@sketis.net>
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
Email Gateway (Aug 17 2022 at 13:45):From: "Achim D. Brucker" <brucker@spamfence.net>
Hi,
Marc Weber <marco-oweber@gmx.de> schrieb:
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
Email Gateway (Aug 17 2022 at 13:45):From: Mark A Hills <mhills@cs.uiuc.edu>
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
Last updated: May 03 2024 at 08:18 UTC