removed obsolete sort 'logic' and '=?=' syntax;
authorwenzelm
Tue, 01 Jun 2004 12:35:46 +0200
changeset 14855 a58abaad4f45
parent 14854 61bdf2ae4dc5
child 14856 669a9a0e7279
removed obsolete sort 'logic' and '=?=' syntax;
src/Pure/Syntax/mixfix.ML
--- a/src/Pure/Syntax/mixfix.ML	Tue Jun 01 12:33:50 2004 +0200
+++ b/src/Pure/Syntax/mixfix.ML	Tue Jun 01 12:35:46 2004 +0200
@@ -266,10 +266,9 @@
   ("_constrain", "['a, type] => 'a",    Mixfix ("_\\<Colon>_", [4, 0], 3)),
   ("_idtyp",   "[id, type] => idt",     Mixfix ("_\\<Colon>_", [], 0)),
   ("_lambda",  "[pttrns, 'a] => logic", Mixfix ("(3\\<lambda>_./ _)", [0, 3], 3)),
-  ("==",       "['a::{}, 'a] => prop",  InfixrName ("\\<equiv>", 2)),
+  ("==",       "['a, 'a] => prop",      InfixrName ("\\<equiv>", 2)),
   ("!!",       "[idts, prop] => prop",  Mixfix ("(3\\<And>_./ _)", [0, 0], 0)),
   ("==>",      "[prop, prop] => prop",  InfixrName ("\\<Longrightarrow>", 1)),
-  ("=?=",      "['a::{}, 'a] => prop",  InfixrName ("\\<equiv>\\<^sup>?", 2)),
   ("_DDDOT",   "aprop",                 Delimfix "\\<dots>"),
   ("_bigimpl", "[asms, prop] => prop",  Mixfix ("((1\\<lbrakk>_\\<rbrakk>)/ \\<Longrightarrow> _)", [0, 1], 1)),
   ("_DDDOT",   "logic",                 Delimfix "\\<dots>")];