Mercurial Mercurial > repos > isabelle / changeset
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | raw | gz | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
uniform notation for == and \<equiv> (cf. 3e3c2af5e8a5);
authorwenzelm
Sun, 30 Dec 2012 16:23:30 +0100
changeset 50636 07f47142378e
parent 50635 5543eff56b16
child 50637 81d6fe75ea5b
uniform notation for == and \<equiv> (cf. 3e3c2af5e8a5);
src/Doc/IsarRef/Inner_Syntax.thy file | annotate | diff | comparison | revisions
src/HOL/Library/Fundamental_Theorem_Algebra.thy file | annotate | diff | comparison | revisions
src/Pure/pure_thy.ML file | annotate | diff | comparison | revisions 
--- 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)"} \\
--- 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)"
--- 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>"),
isabelle