doc-src/Codegen/Thy/Setup.thy
author wenzelm
Wed Aug 22 22:55:41 2012 +0200 (2012-08-22)
changeset 48891 c0eafbd55de3
parent 46517 9d2e682a68eb
permissions -rw-r--r--
prefer ML_file over old uses;
haftmann@28213
     1
theory Setup
haftmann@39066
     2
imports
haftmann@39066
     3
  Complex_Main
haftmann@46517
     4
  "~~/src/HOL/Library/Dlist"
haftmann@46517
     5
  "~~/src/HOL/Library/RBT"
haftmann@46517
     6
  "~~/src/HOL/Library/Mapping"
haftmann@28213
     7
begin
haftmann@28213
     8
wenzelm@48891
     9
ML_file "../../antiquote_setup.ML"
wenzelm@48891
    10
ML_file "../../more_antiquote.ML"
wenzelm@48891
    11
haftmann@38503
    12
setup {*
wenzelm@43564
    13
  Antiquote_Setup.setup #>
wenzelm@43564
    14
  More_Antiquote.setup #>
haftmann@38503
    15
let
haftmann@38503
    16
  val typ = Simple_Syntax.read_typ;
haftmann@38503
    17
in
wenzelm@42293
    18
  Sign.del_modesyntax_i (Symbol.xsymbolsN, false)
wenzelm@42293
    19
   [("_constrain", typ "logic => type => logic", Mixfix ("_\<Colon>_", [4, 0], 3)),
wenzelm@42293
    20
    ("_constrain", typ "prop' => type => prop'", Mixfix ("_\<Colon>_", [4, 0], 3))] #>
wenzelm@42293
    21
  Sign.add_modesyntax_i (Symbol.xsymbolsN, false)
wenzelm@42293
    22
   [("_constrain", typ "logic => type => logic", Mixfix ("_ \<Colon>  _", [4, 0], 3)),
wenzelm@42293
    23
    ("_constrain", typ "prop' => type => prop'", Mixfix ("_ \<Colon> _", [4, 0], 3))]
haftmann@38503
    24
end
haftmann@38503
    25
*}
haftmann@38503
    26
haftmann@34071
    27
setup {* Code_Target.set_default_code_width 74 *}
haftmann@34071
    28
wenzelm@42669
    29
declare [[names_unique = false]]
haftmann@28213
    30
haftmann@28213
    31
end
haftmann@46517
    32