17 |
17 |
18 setup {* |
18 setup {* |
19 let |
19 let |
20 val typ = Simple_Syntax.read_typ; |
20 val typ = Simple_Syntax.read_typ; |
21 in |
21 in |
22 Sign.del_modesyntax (Symbol.xsymbolsN, false) |
22 Sign.del_syntax (Symbol.xsymbolsN, false) |
23 [("_constrain", typ "logic => type => logic", Mixfix ("_\<Colon>_", [4, 0], 3)), |
23 [("_constrain", typ "logic => type => logic", Mixfix ("_\<Colon>_", [4, 0], 3)), |
24 ("_constrain", typ "prop' => type => prop'", Mixfix ("_\<Colon>_", [4, 0], 3))] #> |
24 ("_constrain", typ "prop' => type => prop'", Mixfix ("_\<Colon>_", [4, 0], 3))] #> |
25 Sign.add_modesyntax (Symbol.xsymbolsN, false) |
25 Sign.add_syntax (Symbol.xsymbolsN, false) |
26 [("_constrain", typ "logic => type => logic", Mixfix ("_ \<Colon> _", [4, 0], 3)), |
26 [("_constrain", typ "logic => type => logic", Mixfix ("_ \<Colon> _", [4, 0], 3)), |
27 ("_constrain", typ "prop' => type => prop'", Mixfix ("_ \<Colon> _", [4, 0], 3))] |
27 ("_constrain", typ "prop' => type => prop'", Mixfix ("_ \<Colon> _", [4, 0], 3))] |
28 end |
28 end |
29 *} |
29 *} |
30 |
30 |