haftmann@28213: theory Setup
haftmann@39066: imports
haftmann@39066:   Complex_Main
haftmann@46517:   "~~/src/HOL/Library/Dlist"
haftmann@46517:   "~~/src/HOL/Library/RBT"
haftmann@46517:   "~~/src/HOL/Library/Mapping"
haftmann@30227: uses
haftmann@30227:   "../../antiquote_setup.ML"
haftmann@30227:   "../../more_antiquote.ML"
haftmann@28213: begin
haftmann@28213: 
haftmann@38503: setup {*
wenzelm@43564:   Antiquote_Setup.setup #>
wenzelm@43564:   More_Antiquote.setup #>
haftmann@38503: let
haftmann@38503:   val typ = Simple_Syntax.read_typ;
haftmann@38503: in
wenzelm@42293:   Sign.del_modesyntax_i (Symbol.xsymbolsN, false)
wenzelm@42293:    [("_constrain", typ "logic => type => logic", Mixfix ("_\<Colon>_", [4, 0], 3)),
wenzelm@42293:     ("_constrain", typ "prop' => type => prop'", Mixfix ("_\<Colon>_", [4, 0], 3))] #>
wenzelm@42293:   Sign.add_modesyntax_i (Symbol.xsymbolsN, false)
wenzelm@42293:    [("_constrain", typ "logic => type => logic", Mixfix ("_ \<Colon>  _", [4, 0], 3)),
wenzelm@42293:     ("_constrain", typ "prop' => type => prop'", Mixfix ("_ \<Colon> _", [4, 0], 3))]
haftmann@38503: end
haftmann@38503: *}
haftmann@38503: 
haftmann@34071: setup {* Code_Target.set_default_code_width 74 *}
haftmann@34071: 
wenzelm@42669: declare [[names_unique = false]]
haftmann@28213: 
haftmann@28213: end
haftmann@46517: