# HG changeset patch
# User wenzelm
# Date 857744986 -3600
# Node ID e1d15eabb64d72ae928c84da620448517c25f248
# Parent  3e90c5187ce11603f69ef481c1cd198af7ff8c7c
added \<Colon> syntax for constraints (more compact!);

diff -r 3e90c5187ce1 -r e1d15eabb64d src/Pure/Syntax/mixfix.ML
--- a/src/Pure/Syntax/mixfix.ML	Fri Mar 07 15:28:22 1997 +0100
+++ b/src/Pure/Syntax/mixfix.ML	Fri Mar 07 15:29:46 1997 +0100
@@ -195,6 +195,9 @@
 val pure_sym_syntax =
  [("fun",      "[type, type] => type",  Mixfix ("(_/ \\<Rightarrow> _)", [1, 0], 0)),
   ("_bracket", "[types, type] => type", Mixfix ("([_]/ \\<Rightarrow> _)", [0, 0], 0)),
+  ("_ofsort",  "[tid, sort] => type",   Mixfix ("_\\<Colon>_", [max_pri, 0], max_pri)),
+  ("_constrain", "['a, type] => 'a",    Mixfix ("_\\<Colon>_", [4, 0], 3)),
+  ("_idtyp",   "[id, type] => idt",     Mixfix ("_\\<Colon>_", [], 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)),