removed odd associativity of ==
authornipkow
Wed Dec 19 22:26:26 2012 +0100 (2012-12-19)
changeset 506033e3c2af5e8a5
parent 50599 e129fcc720c1
child 50604 4f840e2e362e
child 50605 620515b73a77
removed odd associativity of ==
src/Pure/Pure.thy
src/Pure/pure_thy.ML
     1.1 --- a/src/Pure/Pure.thy	Wed Dec 19 16:41:55 2012 +0100
     1.2 +++ b/src/Pure/Pure.thy	Wed Dec 19 22:26:26 2012 +0100
     1.3 @@ -146,7 +146,7 @@
     1.4  qed
     1.5  
     1.6  lemma imp_conjunction:
     1.7 -  "(PROP A ==> PROP B &&& PROP C) == (PROP A ==> PROP B) &&& (PROP A ==> PROP C)"
     1.8 +  "(PROP A ==> PROP B &&& PROP C) == ((PROP A ==> PROP B) &&& (PROP A ==> PROP C))"
     1.9  proof
    1.10    assume conj: "PROP A ==> PROP B &&& PROP C"
    1.11    show "(PROP A ==> PROP B) &&& (PROP A ==> PROP C)"
     2.1 --- a/src/Pure/pure_thy.ML	Wed Dec 19 16:41:55 2012 +0100
     2.2 +++ b/src/Pure/pure_thy.ML	Wed Dec 19 22:26:26 2012 +0100
     2.3 @@ -177,7 +177,7 @@
     2.4    #> Sign.add_modesyntax_i ("HTML", false)
     2.5     [("_lambda", typ "pttrns => 'a => logic", Mixfix ("(3\\<lambda>_./ _)", [0, 3], 3))]
     2.6    #> Sign.add_consts_i
     2.7 -   [(Binding.name "==", typ "'a => 'a => prop", Infixr ("==", 2)),
     2.8 +   [(Binding.name "==", typ "'a => 'a => prop", Infix ("==", 2)),
     2.9      (Binding.name "==>", typ "prop => prop => prop", Mixfix ("(_/ ==> _)", [2, 1], 1)),
    2.10      (Binding.name "all", typ "('a => prop) => prop", Binder ("!!", 0, 0)),
    2.11      (Binding.name "prop", typ "prop => prop", NoSyn),