# HG changeset patch
# User wenzelm
# Date 856539330 -3600
# Node ID e2908f8edc8ddb1a8a9fe85ffc959da4f9e84303
# Parent  4385d521a69172d095e420d7a79e96ac8b87f684
tuned symbolic [|_|] syntax;

diff -r 4385d521a691 -r e2908f8edc8d src/Pure/Syntax/mixfix.ML
--- a/src/Pure/Syntax/mixfix.ML	Fri Feb 21 16:28:00 1997 +0100
+++ b/src/Pure/Syntax/mixfix.ML	Fri Feb 21 16:35:30 1997 +0100
@@ -195,7 +195,7 @@
   ("_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)),
+  ("_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))];