doc-src/Codegen/Thy/Setup.thy
author haftmann
Sat Feb 18 20:07:26 2012 +0100 (2012-02-18)
changeset 46517 9d2e682a68eb
parent 43564 9864182c6bad
child 48891 c0eafbd55de3
permissions -rw-r--r--
tuned import
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@30227
     7
uses
haftmann@30227
     8
  "../../antiquote_setup.ML"
haftmann@30227
     9
  "../../more_antiquote.ML"
haftmann@28213
    10
begin
haftmann@28213
    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