# HG changeset patch
# User blanchet
# Date 1300985367 -3600
# Node ID 6066a35f66784ef9adfec339156d1f4066ff3a4a
# Parent  fcfd07f122d4e64881b349f41d3a000b6016f9dc
Metis examples use the new Skolemizer to test it

diff -r fcfd07f122d4 -r 6066a35f6678 src/HOL/Metis_Examples/Abstraction.thy
--- 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)
diff -r fcfd07f122d4 -r 6066a35f6678 src/HOL/Metis_Examples/BT.thy
--- 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"
diff -r fcfd07f122d4 -r 6066a35f6678 src/HOL/Metis_Examples/BigO.thy
--- 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
diff -r fcfd07f122d4 -r 6066a35f6678 src/HOL/Metis_Examples/HO_Reas.thy
--- 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"
diff -r fcfd07f122d4 -r 6066a35f6678 src/HOL/Metis_Examples/Message.thy
--- 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)
 
diff -r fcfd07f122d4 -r 6066a35f6678 src/HOL/Metis_Examples/Tarski.thy
--- 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
diff -r fcfd07f122d4 -r 6066a35f6678 src/HOL/Metis_Examples/set.thy
--- 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))"