--- a/src/HOL/IsaMakefile Wed Dec 15 11:26:28 2010 +0100
+++ b/src/HOL/IsaMakefile Wed Dec 15 11:26:28 2010 +0100
@@ -681,11 +681,11 @@
HOL-Metis_Examples: HOL $(LOG)/HOL-Metis_Examples.gz
-$(LOG)/HOL-Metis_Examples.gz: $(OUT)/HOL Metis_Examples/ROOT.ML \
- Metis_Examples/Abstraction.thy Metis_Examples/BigO.thy \
- Metis_Examples/BT.thy Metis_Examples/Message.thy \
- Metis_Examples/Tarski.thy Metis_Examples/TransClosure.thy \
- Metis_Examples/set.thy
+$(LOG)/HOL-Metis_Examples.gz: $(OUT)/HOL Metis_Examples/ROOT.ML \
+ Metis_Examples/Abstraction.thy Metis_Examples/BigO.thy \
+ Metis_Examples/BT.thy Metis_Examples/HO_Reas.thy \
+ Metis_Examples/Message.thy Metis_Examples/Tarski.thy \
+ Metis_Examples/TransClosure.thy Metis_Examples/set.thy
@$(ISABELLE_TOOL) usedir $(OUT)/HOL Metis_Examples
--- a/src/HOL/Metis_Examples/Abstraction.thy Wed Dec 15 11:26:28 2010 +0100
+++ b/src/HOL/Metis_Examples/Abstraction.thy Wed Dec 15 11:26:28 2010 +0100
@@ -1,7 +1,8 @@
(* Title: HOL/Metis_Examples/Abstraction.thy
Author: Lawrence C Paulson, Cambridge University Computer Laboratory
+ Author: Jasmin Blanchette, TU Muenchen
-Testing the metis method.
+Testing Metis.
*)
theory Abstraction
--- a/src/HOL/Metis_Examples/BT.thy Wed Dec 15 11:26:28 2010 +0100
+++ b/src/HOL/Metis_Examples/BT.thy Wed Dec 15 11:26:28 2010 +0100
@@ -2,7 +2,7 @@
Author: Lawrence C Paulson, Cambridge University Computer Laboratory
Author: Jasmin Blanchette, TU Muenchen
-Testing the metis method
+Testing Metis.
*)
header {* Binary trees *}
--- a/src/HOL/Metis_Examples/BigO.thy Wed Dec 15 11:26:28 2010 +0100
+++ b/src/HOL/Metis_Examples/BigO.thy Wed Dec 15 11:26:28 2010 +0100
@@ -1,7 +1,8 @@
(* Title: HOL/Metis_Examples/BigO.thy
Author: Lawrence C Paulson, Cambridge University Computer Laboratory
+ Author: Jasmin Blanchette, TU Muenchen
-Testing the metis method.
+Testing Metis.
*)
header {* Big O notation *}
--- a/src/HOL/Metis_Examples/HO_Reas.thy Wed Dec 15 11:26:28 2010 +0100
+++ b/src/HOL/Metis_Examples/HO_Reas.thy Wed Dec 15 11:26:28 2010 +0100
@@ -10,24 +10,21 @@
sledgehammer_params [prover = e, blocking, isar_proof, timeout = 10]
-hide_const id
-definition id where "id (x::bool) = x"
-
lemma "id True"
-sledgehammer [expect = some] (add: id_def)
-by (metis id_def)
+sledgehammer [expect = some] (id_apply)
+by (metis id_apply)
lemma "\<not> id False"
-sledgehammer [expect = some] (id_def)
-by (metis id_def)
+sledgehammer [expect = some] (id_apply)
+by (metis id_apply)
lemma "x = id True \<or> x = id False"
-sledgehammer [expect = some] (id_def)
-by (metis id_def)
+sledgehammer [expect = some] (id_apply)
+by (metis id_apply)
lemma "id x = id True \<or> id x = id False"
-sledgehammer [expect = some] (id_def)
-by (metis id_def)
+sledgehammer [expect = some] (id_apply)
+by (metis id_apply)
lemma "P True \<Longrightarrow> P False \<Longrightarrow> P x"
sledgehammer [expect = none] ()
@@ -35,47 +32,47 @@
by metisFT
lemma "id (\<not> a) \<Longrightarrow> \<not> id a"
-sledgehammer [expect = some] (id_def)
-by (metis id_def)
+sledgehammer [expect = some] (id_apply)
+by (metis id_apply)
lemma "id (\<not> \<not> a) \<Longrightarrow> id a"
sledgehammer [expect = some] ()
by metis
lemma "id (\<not> (id (\<not> a))) \<Longrightarrow> id a"
-sledgehammer [expect = some] (id_def)
-by (metis id_def)
+sledgehammer [expect = some] (id_apply)
+by (metis id_apply)
lemma "id (a \<and> b) \<Longrightarrow> id a"
-sledgehammer [expect = some] (id_def)
-by (metis id_def)
+sledgehammer [expect = some] (id_apply)
+by (metis id_apply)
lemma "id (a \<and> b) \<Longrightarrow> id b"
-sledgehammer [expect = some] (id_def)
-by (metis id_def)
+sledgehammer [expect = some] (id_apply)
+by (metis id_apply)
lemma "id a \<Longrightarrow> id b \<Longrightarrow> id (a \<and> b)"
-sledgehammer [expect = some] (id_def)
-by (metis id_def)
+sledgehammer [expect = some] (id_apply)
+by (metis id_apply)
lemma "id a \<Longrightarrow> id (a \<or> b)"
-sledgehammer [expect = some] (id_def)
-by (metis id_def)
+sledgehammer [expect = some] (id_apply)
+by (metis id_apply)
lemma "id b \<Longrightarrow> id (a \<or> b)"
-sledgehammer [expect = some] (id_def)
-by (metis id_def)
+sledgehammer [expect = some] (id_apply)
+by (metis id_apply)
lemma "id (\<not> a) \<Longrightarrow> id (\<not> b) \<Longrightarrow> id (\<not> (a \<or> b))"
-sledgehammer [expect = some] (id_def)
-by (metis id_def)
+sledgehammer [expect = some] (id_apply)
+by (metis id_apply)
lemma "id (\<not> a) \<Longrightarrow> id (a \<longrightarrow> b)"
-sledgehammer [expect = some] (id_def)
-by (metis id_def)
+sledgehammer [expect = some] (id_apply)
+by (metis id_apply)
lemma "id (a \<longrightarrow> b) \<longleftrightarrow> id (\<not> a \<or> b)"
-sledgehammer [expect = some] (id_def)
-by (metis id_def)
+sledgehammer [expect = some] (id_apply)
+by (metis id_apply)
end
--- a/src/HOL/Metis_Examples/Message.thy Wed Dec 15 11:26:28 2010 +0100
+++ b/src/HOL/Metis_Examples/Message.thy Wed Dec 15 11:26:28 2010 +0100
@@ -1,7 +1,8 @@
(* Title: HOL/Metis_Examples/Message.thy
Author: Lawrence C Paulson, Cambridge University Computer Laboratory
+ Author: Jasmin Blanchette, TU Muenchen
-Testing the metis method.
+Testing Metis.
*)
theory Message
--- a/src/HOL/Metis_Examples/ROOT.ML Wed Dec 15 11:26:28 2010 +0100
+++ b/src/HOL/Metis_Examples/ROOT.ML Wed Dec 15 11:26:28 2010 +0100
@@ -5,5 +5,5 @@
Testing Metis and Sledgehammer.
*)
-use_thys ["set", "Abstraction", "BigO", "BT", "HO_Reas", "Message", "Tarski",
- "TransClosure"];
+use_thys ["Abstraction", "BigO", "BT", "HO_Reas", "Message", "Tarski",
+ "TransClosure", "set"];
--- a/src/HOL/Metis_Examples/Tarski.thy Wed Dec 15 11:26:28 2010 +0100
+++ b/src/HOL/Metis_Examples/Tarski.thy Wed Dec 15 11:26:28 2010 +0100
@@ -1,7 +1,8 @@
(* Title: HOL/Metis_Examples/Tarski.thy
Author: Lawrence C Paulson, Cambridge University Computer Laboratory
+ Author: Jasmin Blanchette, TU Muenchen
-Testing the metis method.
+Testing Metis.
*)
header {* The Full Theorem of Tarski *}
--- a/src/HOL/Metis_Examples/TransClosure.thy Wed Dec 15 11:26:28 2010 +0100
+++ b/src/HOL/Metis_Examples/TransClosure.thy Wed Dec 15 11:26:28 2010 +0100
@@ -1,7 +1,8 @@
(* Title: HOL/Metis_Examples/TransClosure.thy
Author: Lawrence C Paulson, Cambridge University Computer Laboratory
+ Author: Jasmin Blanchette, TU Muenchen
-Testing the metis method
+Testing Metis.
*)
theory TransClosure
--- a/src/HOL/Metis_Examples/set.thy Wed Dec 15 11:26:28 2010 +0100
+++ b/src/HOL/Metis_Examples/set.thy Wed Dec 15 11:26:28 2010 +0100
@@ -1,7 +1,8 @@
(* Title: HOL/Metis_Examples/set.thy
Author: Lawrence C Paulson, Cambridge University Computer Laboratory
+ Author: Jasmin Blanchette, TU Muenchen
-Testing the metis method.
+Testing Metis.
*)
theory set