# HG changeset patch
# User ballarin
# Date 1225188187 -3600
# Node ID 32b6a8f12c1cf37617688dde8e1f390d0f6ccbb6
# Parent  b1c4366e1212b4ae46fb92b2fdba496a67690d8f
Removed 'includes meta_term_syntax' and 'includes meta_conjunction_syntax'.

diff -r b1c4366e1212 -r 32b6a8f12c1c src/FOL/FOL.thy
--- a/src/FOL/FOL.thy	Mon Oct 27 18:14:34 2008 +0100
+++ b/src/FOL/FOL.thy	Tue Oct 28 11:03:07 2008 +0100
@@ -347,7 +347,7 @@
   unfolding atomize_eq induct_equal_def .
 
 lemma induct_conj_eq:
-  includes meta_conjunction_syntax
+  fixes meta_conjunction :: "prop => prop => prop"  (infixr "&&" 2)
   shows "(A && B) == Trueprop(induct_conj(A, B))"
   unfolding atomize_conj induct_conj_def .
 
diff -r b1c4366e1212 -r 32b6a8f12c1c src/FOL/IFOL.thy
--- a/src/FOL/IFOL.thy	Mon Oct 27 18:14:34 2008 +0100
+++ b/src/FOL/IFOL.thy	Tue Oct 28 11:03:07 2008 +0100
@@ -699,7 +699,7 @@
 qed
 
 lemma atomize_conj [atomize]:
-  includes meta_conjunction_syntax
+  fixes meta_conjunction :: "prop => prop => prop"  (infixr "&&" 2)
   shows "(A && B) == Trueprop (A & B)"
 proof
   assume conj: "A && B"
diff -r b1c4366e1212 -r 32b6a8f12c1c src/HOL/Code_Setup.thy
--- a/src/HOL/Code_Setup.thy	Mon Oct 27 18:14:34 2008 +0100
+++ b/src/HOL/Code_Setup.thy	Tue Oct 28 11:03:07 2008 +0100
@@ -72,7 +72,7 @@
   using assms by simp_all
 
 lemma If_case_cert:
-  includes meta_conjunction_syntax
+  fixes meta_conjunction :: "prop => prop => prop"  (infixr "&&" 2)
   assumes "CASE \<equiv> (\<lambda>b. If b f g)"
   shows "(CASE True \<equiv> f) && (CASE False \<equiv> g)"
   using assms by simp_all
diff -r b1c4366e1212 -r 32b6a8f12c1c src/HOL/Groebner_Basis.thy
--- a/src/HOL/Groebner_Basis.thy	Mon Oct 27 18:14:34 2008 +0100
+++ b/src/HOL/Groebner_Basis.thy	Tue Oct 28 11:03:07 2008 +0100
@@ -64,7 +64,7 @@
 subsubsection {* Declaring the abstract theory *}
 
 lemma semiring_ops:
-  includes meta_term_syntax
+  fixes meta_term :: "'a => prop"  ("TERM _")
   shows "TERM (add x y)" and "TERM (mul x y)" and "TERM (pwr x n)"
     and "TERM r0" and "TERM r1"
   by rule+
@@ -227,7 +227,7 @@
 begin
 
 lemma ring_ops:
-  includes meta_term_syntax
+  fixes meta_term :: "'a => prop"  ("TERM _")
   shows "TERM (sub x y)" and "TERM (neg x)" .
 
 lemmas ring_rules = neg_mul sub_add
diff -r b1c4366e1212 -r 32b6a8f12c1c src/HOL/HOL.thy
--- a/src/HOL/HOL.thy	Mon Oct 27 18:14:34 2008 +0100
+++ b/src/HOL/HOL.thy	Tue Oct 28 11:03:07 2008 +0100
@@ -846,7 +846,7 @@
 qed
 
 lemma atomize_conj [atomize]:
-  includes meta_conjunction_syntax
+  fixes meta_conjunction :: "prop => prop => prop"  (infixr "&&" 2)
   shows "(A && B) == Trueprop (A & B)"
 proof
   assume conj: "A && B"
@@ -1504,7 +1504,7 @@
   by (unfold atomize_eq induct_equal_def)
 
 lemma induct_conj_eq:
-  includes meta_conjunction_syntax
+  fixes meta_conjunction :: "prop => prop => prop"  (infixr "&&" 2)
   shows "(A && B) == Trueprop (induct_conj A B)"
   by (unfold atomize_conj induct_conj_def)
 
diff -r b1c4366e1212 -r 32b6a8f12c1c src/HOL/Library/Dense_Linear_Order.thy
--- a/src/HOL/Library/Dense_Linear_Order.thy	Mon Oct 27 18:14:34 2008 +0100
+++ b/src/HOL/Library/Dense_Linear_Order.thy	Tue Oct 28 11:03:07 2008 +0100
@@ -268,7 +268,7 @@
 
 lemma axiom: "dense_linear_order (op \<le>) (op <)" by (rule dense_linear_order_axioms)
 lemma atoms:
-  includes meta_term_syntax
+  fixes meta_term :: "'a => prop"  ("TERM _")
   shows "TERM (less :: 'a \<Rightarrow> _)"
     and "TERM (less_eq :: 'a \<Rightarrow> _)"
     and "TERM (op = :: 'a \<Rightarrow> _)" .
@@ -505,7 +505,7 @@
 lemma ferrack_axiom: "constr_dense_linear_order less_eq less between"
   by (rule constr_dense_linear_order_axioms)
 lemma atoms:
-  includes meta_term_syntax
+  fixes meta_term :: "'a => prop"  ("TERM _")
   shows "TERM (less :: 'a \<Rightarrow> _)"
     and "TERM (less_eq :: 'a \<Rightarrow> _)"
     and "TERM (op = :: 'a \<Rightarrow> _)" .
diff -r b1c4366e1212 -r 32b6a8f12c1c src/Pure/Pure.thy
--- a/src/Pure/Pure.thy	Mon Oct 27 18:14:34 2008 +0100
+++ b/src/Pure/Pure.thy	Tue Oct 28 11:03:07 2008 +0100
@@ -38,7 +38,7 @@
   fixes meta_conjunction :: "prop => prop => prop"  (infixr "&&" 2)
 
 lemma all_conjunction:
-  includes meta_conjunction_syntax
+  fixes meta_conjunction :: "prop => prop => prop"  (infixr "&&" 2)
   shows "(!!x. PROP A x && PROP B x) == ((!!x. PROP A x) && (!!x. PROP B x))"
 proof
   assume conj: "!!x. PROP A x && PROP B x"
@@ -59,7 +59,7 @@
 qed
 
 lemma imp_conjunction:
-  includes meta_conjunction_syntax
+  fixes meta_conjunction :: "prop => prop => prop"  (infixr "&&" 2)
   shows "(PROP A ==> PROP B && PROP C) == (PROP A ==> PROP B) && (PROP A ==> PROP C)"
 proof
   assume conj: "PROP A ==> PROP B && PROP C"
@@ -80,7 +80,7 @@
 qed
 
 lemma conjunction_imp:
-  includes meta_conjunction_syntax
+  fixes meta_conjunction :: "prop => prop => prop"  (infixr "&&" 2)
   shows "(PROP A && PROP B ==> PROP C) == (PROP A ==> PROP B ==> PROP C)"
 proof
   assume r: "PROP A && PROP B ==> PROP C"