10 (* type constraints with spacing *) |
10 (* type constraints with spacing *) |
11 setup {* |
11 setup {* |
12 let |
12 let |
13 val typ = Simple_Syntax.read_typ; |
13 val typ = Simple_Syntax.read_typ; |
14 in |
14 in |
15 Sign.del_modesyntax (Symbol.xsymbolsN, false) |
15 Sign.del_syntax (Symbol.xsymbolsN, false) |
16 [("_constrain", typ "logic => type => logic", Mixfix ("_\<Colon>_", [4, 0], 3)), |
16 [("_constrain", typ "logic => type => logic", Mixfix ("_\<Colon>_", [4, 0], 3)), |
17 ("_constrain", typ "prop' => type => prop'", Mixfix ("_\<Colon>_", [4, 0], 3))] #> |
17 ("_constrain", typ "prop' => type => prop'", Mixfix ("_\<Colon>_", [4, 0], 3))] #> |
18 Sign.add_modesyntax (Symbol.xsymbolsN, false) |
18 Sign.add_syntax (Symbol.xsymbolsN, false) |
19 [("_constrain", typ "logic => type => logic", Mixfix ("_ \<Colon> _", [4, 0], 3)), |
19 [("_constrain", typ "logic => type => logic", Mixfix ("_ \<Colon> _", [4, 0], 3)), |
20 ("_constrain", typ "prop' => type => prop'", Mixfix ("_ \<Colon> _", [4, 0], 3))] |
20 ("_constrain", typ "prop' => type => prop'", Mixfix ("_ \<Colon> _", [4, 0], 3))] |
21 end |
21 end |
22 *}(*>*) |
22 *}(*>*) |
23 |
23 |