1.1 --- a/src/FOL/FOL.thy	Mon Oct 27 18:14:34 2008 +0100
     1.2 +++ b/src/FOL/FOL.thy	Tue Oct 28 11:03:07 2008 +0100
     1.3 @@ -347,7 +347,7 @@
     1.4    unfolding atomize_eq induct_equal_def .
     1.5  
     1.6  lemma induct_conj_eq:
     1.7 -  includes meta_conjunction_syntax
     1.8 +  fixes meta_conjunction :: "prop => prop => prop"  (infixr "&&" 2)
     1.9    shows "(A && B) == Trueprop(induct_conj(A, B))"
    1.10    unfolding atomize_conj induct_conj_def .
    1.11  

     2.1 --- a/src/FOL/IFOL.thy	Mon Oct 27 18:14:34 2008 +0100
     2.2 +++ b/src/FOL/IFOL.thy	Tue Oct 28 11:03:07 2008 +0100
     2.3 @@ -699,7 +699,7 @@
     2.4  qed
     2.5  
     2.6  lemma atomize_conj [atomize]:
     2.7 -  includes meta_conjunction_syntax
     2.8 +  fixes meta_conjunction :: "prop => prop => prop"  (infixr "&&" 2)
     2.9    shows "(A && B) == Trueprop (A & B)"
    2.10  proof
    2.11    assume conj: "A && B"

     3.1 --- a/src/HOL/Code_Setup.thy	Mon Oct 27 18:14:34 2008 +0100
     3.2 +++ b/src/HOL/Code_Setup.thy	Tue Oct 28 11:03:07 2008 +0100
     3.3 @@ -72,7 +72,7 @@
     3.4    using assms by simp_all
     3.5  
     3.6  lemma If_case_cert:
     3.7 -  includes meta_conjunction_syntax
     3.8 +  fixes meta_conjunction :: "prop => prop => prop"  (infixr "&&" 2)
     3.9    assumes "CASE \<equiv> (\<lambda>b. If b f g)"
    3.10    shows "(CASE True \<equiv> f) && (CASE False \<equiv> g)"
    3.11    using assms by simp_all

     4.1 --- a/src/HOL/Groebner_Basis.thy	Mon Oct 27 18:14:34 2008 +0100
     4.2 +++ b/src/HOL/Groebner_Basis.thy	Tue Oct 28 11:03:07 2008 +0100
     4.3 @@ -64,7 +64,7 @@
     4.4  subsubsection {* Declaring the abstract theory *}
     4.5  
     4.6  lemma semiring_ops:
     4.7 -  includes meta_term_syntax
     4.8 +  fixes meta_term :: "'a => prop"  ("TERM _")
     4.9    shows "TERM (add x y)" and "TERM (mul x y)" and "TERM (pwr x n)"
    4.10      and "TERM r0" and "TERM r1"
    4.11    by rule+
    4.12 @@ -227,7 +227,7 @@
    4.13  begin
    4.14  
    4.15  lemma ring_ops:
    4.16 -  includes meta_term_syntax
    4.17 +  fixes meta_term :: "'a => prop"  ("TERM _")
    4.18    shows "TERM (sub x y)" and "TERM (neg x)" .
    4.19  
    4.20  lemmas ring_rules = neg_mul sub_add

     5.1 --- a/src/HOL/HOL.thy	Mon Oct 27 18:14:34 2008 +0100
     5.2 +++ b/src/HOL/HOL.thy	Tue Oct 28 11:03:07 2008 +0100
     5.3 @@ -846,7 +846,7 @@
     5.4  qed
     5.5  
     5.6  lemma atomize_conj [atomize]:
     5.7 -  includes meta_conjunction_syntax
     5.8 +  fixes meta_conjunction :: "prop => prop => prop"  (infixr "&&" 2)
     5.9    shows "(A && B) == Trueprop (A & B)"
    5.10  proof
    5.11    assume conj: "A && B"
    5.12 @@ -1504,7 +1504,7 @@
    5.13    by (unfold atomize_eq induct_equal_def)
    5.14  
    5.15  lemma induct_conj_eq:
    5.16 -  includes meta_conjunction_syntax
    5.17 +  fixes meta_conjunction :: "prop => prop => prop"  (infixr "&&" 2)
    5.18    shows "(A && B) == Trueprop (induct_conj A B)"
    5.19    by (unfold atomize_conj induct_conj_def)
    5.20  

     6.1 --- a/src/HOL/Library/Dense_Linear_Order.thy	Mon Oct 27 18:14:34 2008 +0100
     6.2 +++ b/src/HOL/Library/Dense_Linear_Order.thy	Tue Oct 28 11:03:07 2008 +0100
     6.3 @@ -268,7 +268,7 @@
     6.4  
     6.5  lemma axiom: "dense_linear_order (op \<le>) (op <)" by (rule dense_linear_order_axioms)
     6.6  lemma atoms:
     6.7 -  includes meta_term_syntax
     6.8 +  fixes meta_term :: "'a => prop"  ("TERM _")
     6.9    shows "TERM (less :: 'a \<Rightarrow> _)"
    6.10      and "TERM (less_eq :: 'a \<Rightarrow> _)"
    6.11      and "TERM (op = :: 'a \<Rightarrow> _)" .
    6.12 @@ -505,7 +505,7 @@
    6.13  lemma ferrack_axiom: "constr_dense_linear_order less_eq less between"
    6.14    by (rule constr_dense_linear_order_axioms)
    6.15  lemma atoms:
    6.16 -  includes meta_term_syntax
    6.17 +  fixes meta_term :: "'a => prop"  ("TERM _")
    6.18    shows "TERM (less :: 'a \<Rightarrow> _)"
    6.19      and "TERM (less_eq :: 'a \<Rightarrow> _)"
    6.20      and "TERM (op = :: 'a \<Rightarrow> _)" .

     7.1 --- a/src/Pure/Pure.thy	Mon Oct 27 18:14:34 2008 +0100
     7.2 +++ b/src/Pure/Pure.thy	Tue Oct 28 11:03:07 2008 +0100
     7.3 @@ -38,7 +38,7 @@
     7.4    fixes meta_conjunction :: "prop => prop => prop"  (infixr "&&" 2)
     7.5  
     7.6  lemma all_conjunction:
     7.7 -  includes meta_conjunction_syntax
     7.8 +  fixes meta_conjunction :: "prop => prop => prop"  (infixr "&&" 2)
     7.9    shows "(!!x. PROP A x && PROP B x) == ((!!x. PROP A x) && (!!x. PROP B x))"
    7.10  proof
    7.11    assume conj: "!!x. PROP A x && PROP B x"
    7.12 @@ -59,7 +59,7 @@
    7.13  qed
    7.14  
    7.15  lemma imp_conjunction:
    7.16 -  includes meta_conjunction_syntax
    7.17 +  fixes meta_conjunction :: "prop => prop => prop"  (infixr "&&" 2)
    7.18    shows "(PROP A ==> PROP B && PROP C) == (PROP A ==> PROP B) && (PROP A ==> PROP C)"
    7.19  proof
    7.20    assume conj: "PROP A ==> PROP B && PROP C"
    7.21 @@ -80,7 +80,7 @@
    7.22  qed
    7.23  
    7.24  lemma conjunction_imp:
    7.25 -  includes meta_conjunction_syntax
    7.26 +  fixes meta_conjunction :: "prop => prop => prop"  (infixr "&&" 2)
    7.27    shows "(PROP A && PROP B ==> PROP C) == (PROP A ==> PROP B ==> PROP C)"
    7.28  proof
    7.29    assume r: "PROP A && PROP B ==> PROP C"