# HG changeset patch
# User wenzelm
# Date 1356881010 -3600
# Node ID 07f47142378e850ba965bf4af74cb742e370173f
# Parent  5543eff56b161bb1e9bf4529c79de7d5102065eb
uniform notation for == and \<equiv> (cf. 3e3c2af5e8a5);

diff -r 5543eff56b16 -r 07f47142378e src/Doc/IsarRef/Inner_Syntax.thy
--- a/src/Doc/IsarRef/Inner_Syntax.thy	Sat Dec 29 23:15:51 2012 +0100
+++ b/src/Doc/IsarRef/Inner_Syntax.thy	Sun Dec 30 16:23:30 2012 +0100
@@ -740,8 +740,8 @@
 
   @{syntax_def (inner) prop} & = & @{verbatim "("} @{text prop} @{verbatim ")"} \\
     & @{text "|"} & @{text "prop\<^sup>(\<^sup>4\<^sup>)"} @{verbatim "::"} @{text type} & @{text "(3)"} \\
-    & @{text "|"} & @{text "any\<^sup>(\<^sup>3\<^sup>)"} @{verbatim "=="} @{text "any\<^sup>(\<^sup>2\<^sup>)"} & @{text "(2)"} \\
-    & @{text "|"} & @{text "any\<^sup>(\<^sup>3\<^sup>)"} @{text "\<equiv>"} @{text "any\<^sup>(\<^sup>2\<^sup>)"} & @{text "(2)"} \\
+    & @{text "|"} & @{text "any\<^sup>(\<^sup>3\<^sup>)"} @{verbatim "=="} @{text "any\<^sup>(\<^sup>3\<^sup>)"} & @{text "(2)"} \\
+    & @{text "|"} & @{text "any\<^sup>(\<^sup>3\<^sup>)"} @{text "\<equiv>"} @{text "any\<^sup>(\<^sup>3\<^sup>)"} & @{text "(2)"} \\
     & @{text "|"} & @{text "prop\<^sup>(\<^sup>3\<^sup>)"} @{verbatim "&&&"} @{text "prop\<^sup>(\<^sup>2\<^sup>)"} & @{text "(2)"} \\
     & @{text "|"} & @{text "prop\<^sup>(\<^sup>2\<^sup>)"} @{verbatim "==>"} @{text "prop\<^sup>(\<^sup>1\<^sup>)"} & @{text "(1)"} \\
     & @{text "|"} & @{text "prop\<^sup>(\<^sup>2\<^sup>)"} @{text "\<Longrightarrow>"} @{text "prop\<^sup>(\<^sup>1\<^sup>)"} & @{text "(1)"} \\
diff -r 5543eff56b16 -r 07f47142378e src/HOL/Library/Fundamental_Theorem_Algebra.thy
--- a/src/HOL/Library/Fundamental_Theorem_Algebra.thy	Sat Dec 29 23:15:51 2012 +0100
+++ b/src/HOL/Library/Fundamental_Theorem_Algebra.thy	Sun Dec 30 16:23:30 2012 +0100
@@ -1088,7 +1088,7 @@
 
 lemma elim_neg_conv: "- z \<equiv> (-1) * (z::complex)" by simp
 lemma eqT_intr: "PROP P \<Longrightarrow> (True \<Longrightarrow> PROP P )" "PROP P \<Longrightarrow> True" by blast+
-lemma negate_negate_rule: "Trueprop P \<equiv> \<not> P \<equiv> False" by (atomize (full), auto)
+lemma negate_negate_rule: "Trueprop P \<equiv> (\<not> P \<equiv> False)" by (atomize (full), auto)
 
 lemma complex_entire: "(z::complex) \<noteq> 0 \<and> w \<noteq> 0 \<equiv> z*w \<noteq> 0" by simp
 lemma resolve_eq_ne: "(P \<equiv> True) \<equiv> (\<not>P \<equiv> False)" "(P \<equiv> False) \<equiv> (\<not>P \<equiv> True)"
diff -r 5543eff56b16 -r 07f47142378e src/Pure/pure_thy.ML
--- a/src/Pure/pure_thy.ML	Sat Dec 29 23:15:51 2012 +0100
+++ b/src/Pure/pure_thy.ML	Sun Dec 30 16:23:30 2012 +0100
@@ -166,7 +166,7 @@
     ("_idtyp",            typ "id_position => type => idt", Mixfix ("_\\<Colon>_", [], 0)),
     ("_idtypdummy",       typ "type => idt",            Mixfix ("'_()\\<Colon>_", [], 0)),
     ("_lambda",           typ "pttrns => 'a => logic",  Mixfix ("(3\\<lambda>_./ _)", [0, 3], 3)),
-    (const "==",          typ "'a => 'a => prop",       Infixr ("\\<equiv>", 2)),
+    (const "==",          typ "'a => 'a => prop",       Infix ("\\<equiv>", 2)),
     (const "all_binder",  typ "idts => prop => prop",   Mixfix ("(3\\<And>_./ _)", [0, 0], 0)),
     (const "==>",         typ "prop => prop => prop",   Infixr ("\\<Longrightarrow>", 1)),
     ("_DDDOT",            typ "aprop",                  Delimfix "\\<dots>"),