src/HOL/Metis_Examples/Clausification.thy
 changeset 43228 2ed2f092e990 parent 43197 c71657bbdbc0 child 47308 9caab698dbe4
```     1.1 --- a/src/HOL/Metis_Examples/Clausification.thy	Tue Jun 07 07:57:24 2011 +0200
1.2 +++ b/src/HOL/Metis_Examples/Clausification.thy	Tue Jun 07 08:52:35 2011 +0200
1.3 @@ -28,13 +28,13 @@
1.4  by (metis qax)
1.5
1.6  lemma "\<exists>b. \<forall>a. (q b a \<or> q a b)"
1.7 -by (metisFT qax)
1.8 +by (metis (full_types) qax)
1.9
1.10  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.11  by (metis qax)
1.12
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 (metisFT qax)
1.15 +by (metis (full_types) qax)
1.16
1.17  declare [[metis_new_skolemizer]]
1.18
1.19 @@ -42,13 +42,13 @@
1.20  by (metis qax)
1.21
1.22  lemma "\<exists>b. \<forall>a. (q b a \<or> q a b)"
1.23 -by (metisFT qax)
1.24 +by (metis (full_types) qax)
1.25
1.26  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.27  by (metis qax)
1.28
1.29  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.30 -by (metisFT qax)
1.31 +by (metis (full_types) qax)
1.32
1.33  declare [[meson_max_clauses = 60]]
1.34
1.35 @@ -64,7 +64,7 @@
1.36  by (metis rax)
1.37
1.38  lemma "r 0 0 \<or> r 1 1 \<or> r 2 2 \<or> r 3 3"
1.39 -by (metisFT rax)
1.40 +by (metis (full_types) rax)
1.41
1.42  declare [[metis_new_skolemizer]]
1.43
1.44 @@ -72,7 +72,7 @@
1.45  by (metis rax)
1.46
1.47  lemma "r 0 0 \<or> r 1 1 \<or> r 2 2 \<or> r 3 3"
1.48 -by (metisFT rax)
1.49 +by (metis (full_types) rax)
1.50
1.51  lemma "(r 0 0 \<and> r 0 1 \<and> r 0 2 \<and> r 0 3) \<or>
1.52         (r 1 0 \<and> r 1 1 \<and> r 1 2 \<and> r 1 3) \<or>
1.53 @@ -84,7 +84,7 @@
1.54         (r 1 0 \<and> r 1 1 \<and> r 1 2 \<and> r 1 3) \<or>
1.55         (r 2 0 \<and> r 2 1 \<and> r 2 2 \<and> r 2 3) \<or>
1.56         (r 3 0 \<and> r 3 1 \<and> r 3 2 \<and> r 3 3)"
1.57 -by (metisFT rax)
1.58 +by (metis (full_types) rax)
1.59
1.60
1.61  text {* Definitional CNF for goal *}
1.62 @@ -100,7 +100,7 @@
1.63
1.64  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.65                     (p 0 1 \<or> \<not> x) \<and> (p 1 0 \<or> \<not> x) \<and> (p a b \<or> \<not> x)"
1.66 -by (metisFT pax)
1.67 +by (metis (full_types) pax)
1.68
1.69  declare [[metis_new_skolemizer]]
1.70
1.71 @@ -110,7 +110,7 @@
1.72
1.73  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.74                     (p 0 1 \<or> \<not> x) \<and> (p 1 0 \<or> \<not> x) \<and> (p a b \<or> \<not> x)"
1.75 -by (metisFT pax)
1.76 +by (metis (full_types) pax)
1.77
1.78
1.79  text {* New Skolemizer *}
1.80 @@ -134,7 +134,7 @@
1.81    assumes a: "Quotient R Abs Rep"
1.82    shows "symp R"
1.83  using a unfolding Quotient_def using sympI
1.84 -by metisFT
1.85 +by (metis (full_types))
1.86
1.87  lemma
1.88    "(\<exists>x \<in> set xs. P x) \<longleftrightarrow>
```