equal
deleted
inserted
replaced
8 begin |
8 begin |
9 |
9 |
10 setup {* |
10 setup {* |
11 let |
11 let |
12 val typ = Simple_Syntax.read_typ; |
12 val typ = Simple_Syntax.read_typ; |
13 val typeT = Syntax.typeT; |
13 val typeT = Syntax_Ext.typeT; |
14 val spropT = Syntax.spropT; |
14 val spropT = Syntax_Ext.spropT; |
15 in |
15 in |
16 Sign.del_modesyntax_i (Symbol.xsymbolsN, false) [ |
16 Sign.del_modesyntax_i (Symbol.xsymbolsN, false) [ |
17 ("_constrain", typ "logic => type => logic", Mixfix ("_\<Colon>_", [4, 0], 3)), |
17 ("_constrain", typ "logic => type => logic", Mixfix ("_\<Colon>_", [4, 0], 3)), |
18 ("_constrain", [spropT, typeT] ---> spropT, Mixfix ("_\<Colon>_", [4, 0], 3))] |
18 ("_constrain", [spropT, typeT] ---> spropT, Mixfix ("_\<Colon>_", [4, 0], 3))] |
19 #> Sign.add_modesyntax_i (Symbol.xsymbolsN, false) [ |
19 #> Sign.add_modesyntax_i (Symbol.xsymbolsN, false) [ |