tuned symbolic [|_|] syntax;
authorwenzelm
Fri Feb 21 16:35:30 1997 +0100 (1997-02-21)
changeset 2675e2908f8edc8d
parent 2674 4385d521a691
child 2676 585cd2311a98
tuned symbolic [|_|] syntax;
src/Pure/Syntax/mixfix.ML
     1.1 --- a/src/Pure/Syntax/mixfix.ML	Fri Feb 21 16:28:00 1997 +0100
     1.2 +++ b/src/Pure/Syntax/mixfix.ML	Fri Feb 21 16:35:30 1997 +0100
     1.3 @@ -195,7 +195,7 @@
     1.4    ("_bracket", "[types, type] => type",           Mixfix ("([_]/ \\<Rightarrow> _)", [0, 0], 0)),
     1.5    ("_lambda",  "[idts, 'a] => logic",             Mixfix ("(3\\<lambda>_./ _)", [], 0)),
     1.6    ("==>",      "[prop, prop] => prop",            InfixrName ("\\<Midarrow>\\<Rightarrow>", 1)),
     1.7 -  ("_bigimpl", "[asms, prop] => prop",            Mixfix ("((3\\<lbrakk> _ \\<rbrakk>)/ \\<Midarrow>\\<Rightarrow> _)", [0, 1], 1)),
     1.8 +  ("_bigimpl", "[asms, prop] => prop",            Mixfix ("((3\\<lbrakk>_\\<rbrakk>)/ \\<Midarrow>\\<Rightarrow> _)", [0, 1], 1)),
     1.9    ("==",       "['a::{}, 'a] => prop",            InfixrName ("\\<equiv>", 2)),
    1.10    ("!!",       "[idts, prop] => prop",            Mixfix ("(3\\<And>_./ _)", [0, 0], 0))];
    1.11