# HG changeset patch
# User blanchet
# Date 1292408788 -3600
# Node ID 509e51b7509a6afc4626c8fd6000ca39a8056e5b
# Parent  0b05cc14c2cb482447bb70c3aa7ed548a2bdb805
example tuning

diff -r 0b05cc14c2cb -r 509e51b7509a src/HOL/IsaMakefile
--- 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
 
 
diff -r 0b05cc14c2cb -r 509e51b7509a src/HOL/Metis_Examples/Abstraction.thy
--- 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
diff -r 0b05cc14c2cb -r 509e51b7509a src/HOL/Metis_Examples/BT.thy
--- 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 *}
diff -r 0b05cc14c2cb -r 509e51b7509a src/HOL/Metis_Examples/BigO.thy
--- 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 *}
diff -r 0b05cc14c2cb -r 509e51b7509a src/HOL/Metis_Examples/HO_Reas.thy
--- 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
diff -r 0b05cc14c2cb -r 509e51b7509a src/HOL/Metis_Examples/Message.thy
--- 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
diff -r 0b05cc14c2cb -r 509e51b7509a src/HOL/Metis_Examples/ROOT.ML
--- 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"];
diff -r 0b05cc14c2cb -r 509e51b7509a src/HOL/Metis_Examples/Tarski.thy
--- 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 *}
diff -r 0b05cc14c2cb -r 509e51b7509a src/HOL/Metis_Examples/TransClosure.thy
--- 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
diff -r 0b05cc14c2cb -r 509e51b7509a src/HOL/Metis_Examples/set.thy
--- 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