# HG changeset patch
# User wenzelm
# Date 849109316 -3600
# Node ID e9326ab92fbcee306ff41bfe49050f493667d866
# Parent  f9126d306a021969f57e7aeff838065009fa3403
symbol name changes;

diff -r f9126d306a02 -r e9326ab92fbc src/Pure/Syntax/mixfix.ML
--- a/src/Pure/Syntax/mixfix.ML	Wed Nov 27 16:41:27 1996 +0100
+++ b/src/Pure/Syntax/mixfix.ML	Wed Nov 27 16:41:56 1996 +0100
@@ -28,7 +28,7 @@
   val pure_syntax: (string * string * mixfix) list
   val pure_appl_syntax: (string * string * mixfix) list
   val pure_applC_syntax: (string * string * mixfix) list
-  val pure_symfont_syntax: (string * string * mixfix) list
+  val pure_sym_syntax: (string * string * mixfix) list
 end;
 
 signature MIXFIX =
@@ -190,13 +190,13 @@
   ("_applC",     "[('b => 'a), cargs] => logic",  Mixfix ("(1_/ _)", [max_pri, max_pri], max_pri - 1)),
   ("_applC",     "[('b => 'a), cargs] => aprop",  Mixfix ("(1_/ _)", [max_pri, max_pri], max_pri - 1))];
 
-val pure_symfont_syntax =
- [("fun",      "[type, type] => type",            Mixfix ("(_/ \\{Rightarrow} _)", [1, 0], 0)),
-  ("_bracket", "[types, type] => type",           Mixfix ("([_]/ \\{Rightarrow} _)", [0, 0], 0)),
-  ("_lambda",  "[idts, 'a] => logic",             Mixfix ("(3\\{lambda}_./ _)", [], 0)),
-  ("==>",      "[prop, prop] => prop",            InfixrName ("\\{Midarrow}\\{Rightarrow}", 1)),
-  ("_bigimpl", "[asms, prop] => prop",            Mixfix ("((3\\{ldbrak} _ \\{rdbrak})/ \\{Midarrow}\\{Rightarrow} _)", [0, 1], 1)),
-  ("==",       "['a::{}, 'a] => prop",            InfixrName ("\\{equiv}", 2)),
-  ("!!",       "[idts, prop] => prop",            Mixfix ("(3\\{Vee}_./ _)", [0, 0], 0))];
+val pure_sym_syntax =
+ [("fun",      "[type, type] => type",            Mixfix ("(_/ \\<Rightarrow> _)", [1, 0], 0)),
+  ("_bracket", "[types, type] => type",           Mixfix ("([_]/ \\<Rightarrow> _)", [0, 0], 0)),
+  ("_lambda",  "[idts, 'a] => logic",             Mixfix ("(3\\<lambda>_./ _)", [], 0)),
+  ("==>",      "[prop, prop] => prop",            InfixrName ("\\<Midarrow>\\<Rightarrow>", 1)),
+  ("_bigimpl", "[asms, prop] => prop",            Mixfix ("((3\\<lbrakk> _ \\<rbrakk>)/ \\<Midarrow>\\<Rightarrow> _)", [0, 1], 1)),
+  ("==",       "['a::{}, 'a] => prop",            InfixrName ("\\<equiv>", 2)),
+  ("!!",       "[idts, prop] => prop",            Mixfix ("(3\\<And>_./ _)", [0, 0], 0))];
 
 end;