doc-src/Codegen/Thy/Setup.thy
author wenzelm
Tue May 03 22:27:32 2011 +0200 (2011-05-03)
changeset 42669 04dfffda5671
parent 42358 b47d41d9f4b5
child 43271 8b968645d216
permissions -rw-r--r--
more conventional naming scheme: names_long, names_short, names_unique;
haftmann@28213
     1
theory Setup
haftmann@39066
     2
imports
haftmann@39066
     3
  Complex_Main
haftmann@39066
     4
  More_List RBT Dlist Mapping
haftmann@30227
     5
uses
haftmann@30227
     6
  "../../antiquote_setup.ML"
haftmann@30227
     7
  "../../more_antiquote.ML"
haftmann@28213
     8
begin
haftmann@28213
     9
haftmann@38503
    10
setup {*
haftmann@38503
    11
let
haftmann@38503
    12
  val typ = Simple_Syntax.read_typ;
haftmann@38503
    13
in
wenzelm@42293
    14
  Sign.del_modesyntax_i (Symbol.xsymbolsN, false)
wenzelm@42293
    15
   [("_constrain", typ "logic => type => logic", Mixfix ("_\<Colon>_", [4, 0], 3)),
wenzelm@42293
    16
    ("_constrain", typ "prop' => type => prop'", Mixfix ("_\<Colon>_", [4, 0], 3))] #>
wenzelm@42293
    17
  Sign.add_modesyntax_i (Symbol.xsymbolsN, false)
wenzelm@42293
    18
   [("_constrain", typ "logic => type => logic", Mixfix ("_ \<Colon>  _", [4, 0], 3)),
wenzelm@42293
    19
    ("_constrain", typ "prop' => type => prop'", Mixfix ("_ \<Colon> _", [4, 0], 3))]
haftmann@38503
    20
end
haftmann@38503
    21
*}
haftmann@38503
    22
haftmann@34071
    23
setup {* Code_Target.set_default_code_width 74 *}
haftmann@34071
    24
wenzelm@42669
    25
declare [[names_unique = false]]
haftmann@28213
    26
haftmann@28213
    27
end