src/HOL/HOL.thy
changeset 28856 5e009a80fe6d
parent 28741 1b257449f804
child 28952 15a4b2cf8c34
     1.1 --- a/src/HOL/HOL.thy	Wed Nov 19 18:15:31 2008 +0100
     1.2 +++ b/src/HOL/HOL.thy	Thu Nov 20 00:03:47 2008 +0100
     1.3 @@ -845,11 +845,9 @@
     1.4    then show "x == y" by (rule eq_reflection)
     1.5  qed
     1.6  
     1.7 -lemma atomize_conj [atomize]:
     1.8 -  fixes meta_conjunction :: "prop => prop => prop"  (infixr "&&" 2)
     1.9 -  shows "(A && B) == Trueprop (A & B)"
    1.10 +lemma atomize_conj [atomize]: "(A &&& B) == Trueprop (A & B)"
    1.11  proof
    1.12 -  assume conj: "A && B"
    1.13 +  assume conj: "A &&& B"
    1.14    show "A & B"
    1.15    proof (rule conjI)
    1.16      from conj show A by (rule conjunctionD1)
    1.17 @@ -857,7 +855,7 @@
    1.18    qed
    1.19  next
    1.20    assume conj: "A & B"
    1.21 -  show "A && B"
    1.22 +  show "A &&& B"
    1.23    proof -
    1.24      from conj show A ..
    1.25      from conj show B ..
    1.26 @@ -1511,9 +1509,7 @@
    1.27  lemma induct_equal_eq: "(x == y) == Trueprop (induct_equal x y)"
    1.28    by (unfold atomize_eq induct_equal_def)
    1.29  
    1.30 -lemma induct_conj_eq:
    1.31 -  fixes meta_conjunction :: "prop => prop => prop"  (infixr "&&" 2)
    1.32 -  shows "(A && B) == Trueprop (induct_conj A B)"
    1.33 +lemma induct_conj_eq: "(A &&& B) == Trueprop (induct_conj A B)"
    1.34    by (unfold atomize_conj induct_conj_def)
    1.35  
    1.36  lemmas induct_atomize = induct_forall_eq induct_implies_eq induct_equal_eq induct_conj_eq