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
```