Reduced space for xsymbols output of [| |] ==> from 3 to 1
authornipkow
Tue, 27 Jan 2004 08:15:10 +0100
changeset 14363 2c116016f95d
parent 14362 b378b6faf4a7
child 14364 fc62df0bf353
Reduced space for xsymbols output of [| |] ==> from 3 to 1
src/Pure/Syntax/mixfix.ML
--- a/src/Pure/Syntax/mixfix.ML	Mon Jan 26 15:33:51 2004 +0100
+++ b/src/Pure/Syntax/mixfix.ML	Tue Jan 27 08:15:10 2004 +0100
@@ -269,7 +269,7 @@
   ("==>",      "[prop, prop] => prop",  InfixrName ("\\<Longrightarrow>", 1)),
   ("=?=",      "['a::{}, 'a] => prop",  InfixrName ("\\<equiv>\\<^sup>?", 2)),
   ("_DDDOT",   "aprop",                 Delimfix "\\<dots>"),
-  ("_bigimpl", "[asms, prop] => prop",  Mixfix ("((3\\<lbrakk>_\\<rbrakk>)/ \\<Longrightarrow> _)", [0, 1], 1)),
+  ("_bigimpl", "[asms, prop] => prop",  Mixfix ("((1\\<lbrakk>_\\<rbrakk>)/ \\<Longrightarrow> _)", [0, 1], 1)),
   ("_DDDOT",   "logic",                 Delimfix "\\<dots>")];
 
 end;