src/Doc/Codegen/Setup.thy
author haftmann
Fri Jan 09 08:37:00 2015 +0100 (2015-01-09)
changeset 59324 f5f9993a168d
parent 56240 938c6c7e10eb
child 59334 f0141b991c8f
permissions -rw-r--r--
prefer option for default code printing width
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@56208
    12
  Isabelle_System.mkdirs (Path.append (Resources.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 {*
haftmann@38503
    19
let
haftmann@38503
    20
  val typ = Simple_Syntax.read_typ;
haftmann@38503
    21
in
wenzelm@56240
    22
  Sign.del_syntax (Symbol.xsymbolsN, false)
wenzelm@42293
    23
   [("_constrain", typ "logic => type => logic", Mixfix ("_\<Colon>_", [4, 0], 3)),
wenzelm@42293
    24
    ("_constrain", typ "prop' => type => prop'", Mixfix ("_\<Colon>_", [4, 0], 3))] #>
wenzelm@56240
    25
  Sign.add_syntax (Symbol.xsymbolsN, false)
wenzelm@42293
    26
   [("_constrain", typ "logic => type => logic", Mixfix ("_ \<Colon>  _", [4, 0], 3)),
wenzelm@42293
    27
    ("_constrain", typ "prop' => type => prop'", Mixfix ("_ \<Colon> _", [4, 0], 3))]
haftmann@38503
    28
end
haftmann@38503
    29
*}
haftmann@38503
    30
haftmann@59324
    31
declare [[default_code_width = 74]]
haftmann@34071
    32
wenzelm@42669
    33
declare [[names_unique = false]]
haftmann@28213
    34
haftmann@28213
    35
end