src/Doc/Codegen/Setup.thy
author haftmann
Fri Feb 15 12:48:20 2013 +0100 (2013-02-15)
changeset 51162 310b94ed1815
parent 48985 5386df44a037
child 56059 2390391584c2
permissions -rw-r--r--
dropped now obsolete hint;
a few words on theory IArray;
dropped reference to obsolete theory Efficient_Nat
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@51162
     7
  "~~/src/HOL/Library/IArray"
haftmann@28213
     8
begin
haftmann@28213
     9
wenzelm@48951
    10
(* FIXME avoid writing into source directory *)
wenzelm@48951
    11
ML {*
wenzelm@48951
    12
  Isabelle_System.mkdirs (Path.append (Thy_Load.master_directory @{theory}) (Path.basic "examples"))
wenzelm@48951
    13
*}
wenzelm@48951
    14
wenzelm@48951
    15
ML_file "../antiquote_setup.ML"
wenzelm@48951
    16
ML_file "../more_antiquote.ML"
wenzelm@48891
    17
haftmann@38503
    18
setup {*
wenzelm@43564
    19
  Antiquote_Setup.setup #>
wenzelm@43564
    20
  More_Antiquote.setup #>
haftmann@38503
    21
let
haftmann@38503
    22
  val typ = Simple_Syntax.read_typ;
haftmann@38503
    23
in
wenzelm@42293
    24
  Sign.del_modesyntax_i (Symbol.xsymbolsN, false)
wenzelm@42293
    25
   [("_constrain", typ "logic => type => logic", Mixfix ("_\<Colon>_", [4, 0], 3)),
wenzelm@42293
    26
    ("_constrain", typ "prop' => type => prop'", Mixfix ("_\<Colon>_", [4, 0], 3))] #>
wenzelm@42293
    27
  Sign.add_modesyntax_i (Symbol.xsymbolsN, false)
wenzelm@42293
    28
   [("_constrain", typ "logic => type => logic", Mixfix ("_ \<Colon>  _", [4, 0], 3)),
wenzelm@42293
    29
    ("_constrain", typ "prop' => type => prop'", Mixfix ("_ \<Colon> _", [4, 0], 3))]
haftmann@38503
    30
end
haftmann@38503
    31
*}
haftmann@38503
    32
haftmann@34071
    33
setup {* Code_Target.set_default_code_width 74 *}
haftmann@34071
    34
wenzelm@42669
    35
declare [[names_unique = false]]
haftmann@28213
    36
haftmann@28213
    37
end
haftmann@46517
    38