# HG changeset patch
# User nipkow
# Date 1355952386 -3600
# Node ID 3e3c2af5e8a52cac94e1c4a19a20bec4ba8484a7
# Parent  e129fcc720c1e068923e5ff6b980703be26443f2
removed odd associativity of ==

diff -r e129fcc720c1 -r 3e3c2af5e8a5 src/Pure/Pure.thy
--- a/src/Pure/Pure.thy	Wed Dec 19 16:41:55 2012 +0100
+++ b/src/Pure/Pure.thy	Wed Dec 19 22:26:26 2012 +0100
@@ -146,7 +146,7 @@
 qed
 
 lemma imp_conjunction:
-  "(PROP A ==> PROP B &&& PROP C) == (PROP A ==> PROP B) &&& (PROP A ==> PROP C)"
+  "(PROP A ==> PROP B &&& PROP C) == ((PROP A ==> PROP B) &&& (PROP A ==> PROP C))"
 proof
   assume conj: "PROP A ==> PROP B &&& PROP C"
   show "(PROP A ==> PROP B) &&& (PROP A ==> PROP C)"
diff -r e129fcc720c1 -r 3e3c2af5e8a5 src/Pure/pure_thy.ML
--- a/src/Pure/pure_thy.ML	Wed Dec 19 16:41:55 2012 +0100
+++ b/src/Pure/pure_thy.ML	Wed Dec 19 22:26:26 2012 +0100
@@ -177,7 +177,7 @@
   #> Sign.add_modesyntax_i ("HTML", false)
    [("_lambda", typ "pttrns => 'a => logic", Mixfix ("(3\\<lambda>_./ _)", [0, 3], 3))]
   #> Sign.add_consts_i
-   [(Binding.name "==", typ "'a => 'a => prop", Infixr ("==", 2)),
+   [(Binding.name "==", typ "'a => 'a => prop", Infix ("==", 2)),
     (Binding.name "==>", typ "prop => prop => prop", Mixfix ("(_/ ==> _)", [2, 1], 1)),
     (Binding.name "all", typ "('a => prop) => prop", Binder ("!!", 0, 0)),
     (Binding.name "prop", typ "prop => prop", NoSyn),