src/HOL/HOL.thy
changeset 28699 32b6a8f12c1c
parent 28682 5de9fc98ad96
child 28741 1b257449f804
     1.1 --- a/src/HOL/HOL.thy	Mon Oct 27 18:14:34 2008 +0100
     1.2 +++ b/src/HOL/HOL.thy	Tue Oct 28 11:03:07 2008 +0100
     1.3 @@ -846,7 +846,7 @@
     1.4  qed
     1.5  
     1.6  lemma atomize_conj [atomize]:
     1.7 -  includes meta_conjunction_syntax
     1.8 +  fixes meta_conjunction :: "prop => prop => prop"  (infixr "&&" 2)
     1.9    shows "(A && B) == Trueprop (A & B)"
    1.10  proof
    1.11    assume conj: "A && B"
    1.12 @@ -1504,7 +1504,7 @@
    1.13    by (unfold atomize_eq induct_equal_def)
    1.14  
    1.15  lemma induct_conj_eq:
    1.16 -  includes meta_conjunction_syntax
    1.17 +  fixes meta_conjunction :: "prop => prop => prop"  (infixr "&&" 2)
    1.18    shows "(A && B) == Trueprop (induct_conj A B)"
    1.19    by (unfold atomize_conj induct_conj_def)
    1.20