Mercurial Mercurial > repos > isabelle / changeset
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | raw | gz | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
added \<Colon> syntax for constraints (more compact!);
authorwenzelm
Fri, 07 Mar 1997 15:29:46 +0100
changeset 2767 e1d15eabb64d
parent 2766 3e90c5187ce1
child 2768 bc6d915b8019
added \<Colon> syntax for constraints (more compact!);
src/Pure/Syntax/mixfix.ML file | annotate | diff | comparison | revisions 
--- 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)),
isabelle