doc-src/Codegen/Thy/Setup.thy
changeset 43564 9864182c6bad
parent 43271 8b968645d216
child 46517 9d2e682a68eb
equal deleted inserted replaced
43563:aeabb735883a 43564:9864182c6bad
     6   "../../antiquote_setup.ML"
     6   "../../antiquote_setup.ML"
     7   "../../more_antiquote.ML"
     7   "../../more_antiquote.ML"
     8 begin
     8 begin
     9 
     9 
    10 setup {*
    10 setup {*
       
    11   Antiquote_Setup.setup #>
       
    12   More_Antiquote.setup #>
    11 let
    13 let
    12   val typ = Simple_Syntax.read_typ;
    14   val typ = Simple_Syntax.read_typ;
    13 in
    15 in
    14   Sign.del_modesyntax_i (Symbol.xsymbolsN, false)
    16   Sign.del_modesyntax_i (Symbol.xsymbolsN, false)
    15    [("_constrain", typ "logic => type => logic", Mixfix ("_\<Colon>_", [4, 0], 3)),
    17    [("_constrain", typ "logic => type => logic", Mixfix ("_\<Colon>_", [4, 0], 3)),