--- a/src/HOL/Metis_Examples/Abstraction.thy Thu Mar 24 17:49:27 2011 +0100
+++ b/src/HOL/Metis_Examples/Abstraction.thy Thu Mar 24 17:49:27 2011 +0100
@@ -9,6 +9,8 @@
imports Main "~~/src/HOL/Library/FuncSet"
begin
+declare [[metis_new_skolemizer]]
+
(*For Christoph Benzmueller*)
lemma "x<1 & ((op=) = (op=)) ==> ((op=) = (op=)) & (x<(2::nat))";
by (metis One_nat_def less_Suc0 not_less0 not_less_eq numeral_2_eq_2)
--- a/src/HOL/Metis_Examples/BT.thy Thu Mar 24 17:49:27 2011 +0100
+++ b/src/HOL/Metis_Examples/BT.thy Thu Mar 24 17:49:27 2011 +0100
@@ -11,6 +11,8 @@
imports Main
begin
+declare [[metis_new_skolemizer]]
+
datatype 'a bt =
Lf
| Br 'a "'a bt" "'a bt"
--- a/src/HOL/Metis_Examples/BigO.thy Thu Mar 24 17:49:27 2011 +0100
+++ b/src/HOL/Metis_Examples/BigO.thy Thu Mar 24 17:49:27 2011 +0100
@@ -15,6 +15,8 @@
"~~/src/HOL/Library/Set_Algebras"
begin
+declare [[metis_new_skolemizer]]
+
subsection {* Definitions *}
definition bigo :: "('a => 'b::linordered_idom) => ('a => 'b) set" ("(1O'(_'))") where
--- a/src/HOL/Metis_Examples/HO_Reas.thy Thu Mar 24 17:49:27 2011 +0100
+++ b/src/HOL/Metis_Examples/HO_Reas.thy Thu Mar 24 17:49:27 2011 +0100
@@ -8,6 +8,8 @@
imports Main
begin
+declare [[metis_new_skolemizer]]
+
sledgehammer_params [prover = e, blocking, isar_proof, timeout = 10]
lemma "id True"
--- a/src/HOL/Metis_Examples/Message.thy Thu Mar 24 17:49:27 2011 +0100
+++ b/src/HOL/Metis_Examples/Message.thy Thu Mar 24 17:49:27 2011 +0100
@@ -9,6 +9,8 @@
imports Main
begin
+declare [[metis_new_skolemizer]]
+
lemma strange_Un_eq [simp]: "A \<union> (B \<union> A) = B \<union> A"
by (metis Un_commute Un_left_absorb)
--- a/src/HOL/Metis_Examples/Tarski.thy Thu Mar 24 17:49:27 2011 +0100
+++ b/src/HOL/Metis_Examples/Tarski.thy Thu Mar 24 17:49:27 2011 +0100
@@ -11,6 +11,8 @@
imports Main "~~/src/HOL/Library/FuncSet"
begin
+declare [[metis_new_skolemizer]]
+
(*Many of these higher-order problems appear to be impossible using the
current linkup. They often seem to need either higher-order unification
or explicit reasoning about connectives such as conjunction. The numerous
--- a/src/HOL/Metis_Examples/set.thy Thu Mar 24 17:49:27 2011 +0100
+++ b/src/HOL/Metis_Examples/set.thy Thu Mar 24 17:49:27 2011 +0100
@@ -9,6 +9,8 @@
imports Main
begin
+declare [[metis_new_skolemizer]]
+
lemma "EX x X. ALL y. EX z Z. (~P(y,y) | P(x,x) | ~S(z,x)) &
(S(x,y) | ~S(y,z) | Q(Z,Z)) &
(Q(X,y) | ~Q(y,Z) | S(X,X))"