src/Pure/Pure.thy
changeset 28699 32b6a8f12c1c
parent 27681 8cedebf55539
child 28856 5e009a80fe6d
     1.1 --- a/src/Pure/Pure.thy	Mon Oct 27 18:14:34 2008 +0100
     1.2 +++ b/src/Pure/Pure.thy	Tue Oct 28 11:03:07 2008 +0100
     1.3 @@ -38,7 +38,7 @@
     1.4    fixes meta_conjunction :: "prop => prop => prop"  (infixr "&&" 2)
     1.5  
     1.6  lemma all_conjunction:
     1.7 -  includes meta_conjunction_syntax
     1.8 +  fixes meta_conjunction :: "prop => prop => prop"  (infixr "&&" 2)
     1.9    shows "(!!x. PROP A x && PROP B x) == ((!!x. PROP A x) && (!!x. PROP B x))"
    1.10  proof
    1.11    assume conj: "!!x. PROP A x && PROP B x"
    1.12 @@ -59,7 +59,7 @@
    1.13  qed
    1.14  
    1.15  lemma imp_conjunction:
    1.16 -  includes meta_conjunction_syntax
    1.17 +  fixes meta_conjunction :: "prop => prop => prop"  (infixr "&&" 2)
    1.18    shows "(PROP A ==> PROP B && PROP C) == (PROP A ==> PROP B) && (PROP A ==> PROP C)"
    1.19  proof
    1.20    assume conj: "PROP A ==> PROP B && PROP C"
    1.21 @@ -80,7 +80,7 @@
    1.22  qed
    1.23  
    1.24  lemma conjunction_imp:
    1.25 -  includes meta_conjunction_syntax
    1.26 +  fixes meta_conjunction :: "prop => prop => prop"  (infixr "&&" 2)
    1.27    shows "(PROP A && PROP B ==> PROP C) == (PROP A ==> PROP B ==> PROP C)"
    1.28  proof
    1.29    assume r: "PROP A && PROP B ==> PROP C"