changed syntax "(| _ : _ |)" to "OFCLASS(_, _)";
authorwenzelm
Thu, 14 Jul 1994 11:37:08 +0200
changeset 472 bbaa2a02bd82
parent 471 22325fd7234e
child 473 fdacecc688a1
changed syntax "(| _ : _ |)" to "OFCLASS(_, _)";
src/Pure/Syntax/mixfix.ML
--- a/src/Pure/Syntax/mixfix.ML	Wed Jul 13 10:13:52 1994 +0200
+++ b/src/Pure/Syntax/mixfix.ML	Thu Jul 14 11:37:08 1994 +0200
@@ -164,7 +164,7 @@
   ("",          "prop => asms",                   Delimfix "_"),
   ("_asms",     "[prop, asms] => asms",           Delimfix "_;/ _"),
   ("_bigimpl",  "[asms, prop] => prop",           Mixfix ("((3[| _ |]) ==>/ _)", [0, 1], 1)),
-  ("_insort",   "[type, 'a] => prop",             Delimfix "(2'(| _ :/ _ |'))"),
+  ("_ofclass",  "[type, 'a] => prop",             Delimfix "(1OFCLASS/(1'(_,/ _')))"),
   ("_K",        "'a",                             NoSyn),
   ("_explode",  "'a",                             NoSyn),
   ("_implode",  "'a",                             NoSyn)];