src/HOL/Metis_Examples/Clausification.thy
 changeset 50705 0e943b33d907 parent 50696 85f944352d55 child 55417 01fbfb60c33e
```     1.1 --- a/src/HOL/Metis_Examples/Clausification.thy	Thu Jan 03 17:10:12 2013 +0100
1.2 +++ b/src/HOL/Metis_Examples/Clausification.thy	Thu Jan 03 17:28:55 2013 +0100
1.3 @@ -18,7 +18,7 @@
1.4  axiomatization q :: "nat \<Rightarrow> nat \<Rightarrow> bool" where
1.5  qax: "\<exists>b. \<forall>a. (q b a \<and> q 0 0 \<and> q 1 a \<and> q a 1) \<or> (q 0 1 \<and> q 1 0 \<and> q a b \<and> q 1 1)"
1.6
1.7 -declare [[metis_new_skolemizer = false]]
1.8 +declare [[metis_new_skolem = false]]
1.9
1.10  lemma "\<exists>b. \<forall>a. (q b a \<or> q a b)"
1.11  by (metis qax)
1.12 @@ -32,7 +32,7 @@
1.13  lemma "\<exists>b. \<forall>a. (q b a \<and> q 0 0 \<and> q 1 a \<and> q a 1) \<or> (q 0 1 \<and> q 1 0 \<and> q a b \<and> q 1 1)"
1.14  by (metis (full_types) qax)
1.15
1.16 -declare [[metis_new_skolemizer]]
1.17 +declare [[metis_new_skolem]]
1.18
1.19  lemma "\<exists>b. \<forall>a. (q b a \<or> q a b)"
1.20  by (metis qax)
1.21 @@ -54,7 +54,7 @@
1.22        (r 2 0 \<and> r 2 1 \<and> r 2 2 \<and> r 2 3) \<or>
1.23        (r 3 0 \<and> r 3 1 \<and> r 3 2 \<and> r 3 3)"
1.24
1.25 -declare [[metis_new_skolemizer = false]]
1.26 +declare [[metis_new_skolem = false]]
1.27
1.28  lemma "r 0 0 \<or> r 1 1 \<or> r 2 2 \<or> r 3 3"
1.29  by (metis rax)
1.30 @@ -62,7 +62,7 @@
1.31  lemma "r 0 0 \<or> r 1 1 \<or> r 2 2 \<or> r 3 3"
1.32  by (metis (full_types) rax)
1.33
1.34 -declare [[metis_new_skolemizer]]
1.35 +declare [[metis_new_skolem]]
1.36
1.37  lemma "r 0 0 \<or> r 1 1 \<or> r 2 2 \<or> r 3 3"
1.38  by (metis rax)
1.39 @@ -88,7 +88,7 @@
1.40  axiomatization p :: "nat \<Rightarrow> nat \<Rightarrow> bool" where
1.41  pax: "\<exists>b. \<forall>a. (p b a \<and> p 0 0 \<and> p 1 a) \<or> (p 0 1 \<and> p 1 0 \<and> p a b)"
1.42
1.43 -declare [[metis_new_skolemizer = false]]
1.44 +declare [[metis_new_skolem = false]]
1.45
1.46  lemma "\<exists>b. \<forall>a. \<exists>x. (p b a \<or> x) \<and> (p 0 0 \<or> x) \<and> (p 1 a \<or> x) \<and>
1.47                     (p 0 1 \<or> \<not> x) \<and> (p 1 0 \<or> \<not> x) \<and> (p a b \<or> \<not> x)"
1.48 @@ -98,7 +98,7 @@
1.49                     (p 0 1 \<or> \<not> x) \<and> (p 1 0 \<or> \<not> x) \<and> (p a b \<or> \<not> x)"
1.50  by (metis (full_types) pax)
1.51
1.52 -declare [[metis_new_skolemizer]]
1.53 +declare [[metis_new_skolem]]
1.54
1.55  lemma "\<exists>b. \<forall>a. \<exists>x. (p b a \<or> x) \<and> (p 0 0 \<or> x) \<and> (p 1 a \<or> x) \<and>
1.56                     (p 0 1 \<or> \<not> x) \<and> (p 1 0 \<or> \<not> x) \<and> (p a b \<or> \<not> x)"
1.57 @@ -111,7 +111,7 @@
1.58
1.59  text {* New Skolemizer *}
1.60
1.61 -declare [[metis_new_skolemizer]]
1.62 +declare [[metis_new_skolem]]
1.63
1.64  lemma
1.65    fixes x :: real
```