uniform notation for == and \<equiv> (cf. 3e3c2af5e8a5);
authorwenzelm
Sun Dec 30 16:23:30 2012 +0100 (2012-12-30)
changeset 5063607f47142378e
parent 50635 5543eff56b16
child 50637 81d6fe75ea5b
uniform notation for == and \<equiv> (cf. 3e3c2af5e8a5);
src/Doc/IsarRef/Inner_Syntax.thy
src/HOL/Library/Fundamental_Theorem_Algebra.thy
src/Pure/pure_thy.ML
     1.1 --- a/src/Doc/IsarRef/Inner_Syntax.thy	Sat Dec 29 23:15:51 2012 +0100
     1.2 +++ b/src/Doc/IsarRef/Inner_Syntax.thy	Sun Dec 30 16:23:30 2012 +0100
     1.3 @@ -740,8 +740,8 @@
     1.4  
     1.5    @{syntax_def (inner) prop} & = & @{verbatim "("} @{text prop} @{verbatim ")"} \\
     1.6      & @{text "|"} & @{text "prop\<^sup>(\<^sup>4\<^sup>)"} @{verbatim "::"} @{text type} & @{text "(3)"} \\
     1.7 -    & @{text "|"} & @{text "any\<^sup>(\<^sup>3\<^sup>)"} @{verbatim "=="} @{text "any\<^sup>(\<^sup>2\<^sup>)"} & @{text "(2)"} \\
     1.8 -    & @{text "|"} & @{text "any\<^sup>(\<^sup>3\<^sup>)"} @{text "\<equiv>"} @{text "any\<^sup>(\<^sup>2\<^sup>)"} & @{text "(2)"} \\
     1.9 +    & @{text "|"} & @{text "any\<^sup>(\<^sup>3\<^sup>)"} @{verbatim "=="} @{text "any\<^sup>(\<^sup>3\<^sup>)"} & @{text "(2)"} \\
    1.10 +    & @{text "|"} & @{text "any\<^sup>(\<^sup>3\<^sup>)"} @{text "\<equiv>"} @{text "any\<^sup>(\<^sup>3\<^sup>)"} & @{text "(2)"} \\
    1.11      & @{text "|"} & @{text "prop\<^sup>(\<^sup>3\<^sup>)"} @{verbatim "&&&"} @{text "prop\<^sup>(\<^sup>2\<^sup>)"} & @{text "(2)"} \\
    1.12      & @{text "|"} & @{text "prop\<^sup>(\<^sup>2\<^sup>)"} @{verbatim "==>"} @{text "prop\<^sup>(\<^sup>1\<^sup>)"} & @{text "(1)"} \\
    1.13      & @{text "|"} & @{text "prop\<^sup>(\<^sup>2\<^sup>)"} @{text "\<Longrightarrow>"} @{text "prop\<^sup>(\<^sup>1\<^sup>)"} & @{text "(1)"} \\
     2.1 --- a/src/HOL/Library/Fundamental_Theorem_Algebra.thy	Sat Dec 29 23:15:51 2012 +0100
     2.2 +++ b/src/HOL/Library/Fundamental_Theorem_Algebra.thy	Sun Dec 30 16:23:30 2012 +0100
     2.3 @@ -1088,7 +1088,7 @@
     2.4  
     2.5  lemma elim_neg_conv: "- z \<equiv> (-1) * (z::complex)" by simp
     2.6  lemma eqT_intr: "PROP P \<Longrightarrow> (True \<Longrightarrow> PROP P )" "PROP P \<Longrightarrow> True" by blast+
     2.7 -lemma negate_negate_rule: "Trueprop P \<equiv> \<not> P \<equiv> False" by (atomize (full), auto)
     2.8 +lemma negate_negate_rule: "Trueprop P \<equiv> (\<not> P \<equiv> False)" by (atomize (full), auto)
     2.9  
    2.10  lemma complex_entire: "(z::complex) \<noteq> 0 \<and> w \<noteq> 0 \<equiv> z*w \<noteq> 0" by simp
    2.11  lemma resolve_eq_ne: "(P \<equiv> True) \<equiv> (\<not>P \<equiv> False)" "(P \<equiv> False) \<equiv> (\<not>P \<equiv> True)"
     3.1 --- a/src/Pure/pure_thy.ML	Sat Dec 29 23:15:51 2012 +0100
     3.2 +++ b/src/Pure/pure_thy.ML	Sun Dec 30 16:23:30 2012 +0100
     3.3 @@ -166,7 +166,7 @@
     3.4      ("_idtyp",            typ "id_position => type => idt", Mixfix ("_\\<Colon>_", [], 0)),
     3.5      ("_idtypdummy",       typ "type => idt",            Mixfix ("'_()\\<Colon>_", [], 0)),
     3.6      ("_lambda",           typ "pttrns => 'a => logic",  Mixfix ("(3\\<lambda>_./ _)", [0, 3], 3)),
     3.7 -    (const "==",          typ "'a => 'a => prop",       Infixr ("\\<equiv>", 2)),
     3.8 +    (const "==",          typ "'a => 'a => prop",       Infix ("\\<equiv>", 2)),
     3.9      (const "all_binder",  typ "idts => prop => prop",   Mixfix ("(3\\<And>_./ _)", [0, 0], 0)),
    3.10      (const "==>",         typ "prop => prop => prop",   Infixr ("\\<Longrightarrow>", 1)),
    3.11      ("_DDDOT",            typ "aprop",                  Delimfix "\\<dots>"),