src/Doc/Codegen/Setup.thy
author wenzelm
Wed, 09 Sep 2015 14:47:41 +0200
changeset 61143 5f898411ce87
parent 59378 065f349852e6
child 61670 301e0b4ecd45
permissions -rw-r--r--
eliminated \<Colon> from syntax of constraints;
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
28213
b52f9205a02d New outline for codegen tutorial -- draft
haftmann
parents:
diff changeset
     1
theory Setup
39066
4517a4049588 more canonical theory setup
haftmann
parents: 38798
diff changeset
     2
imports
4517a4049588 more canonical theory setup
haftmann
parents: 38798
diff changeset
     3
  Complex_Main
59378
065f349852e6 separate image for prerequisites of codegen tutorial
haftmann
parents: 59377
diff changeset
     4
  "~~/src/Tools/Permanent_Interpretation"
46517
9d2e682a68eb tuned import
haftmann
parents: 43564
diff changeset
     5
  "~~/src/HOL/Library/Dlist"
9d2e682a68eb tuned import
haftmann
parents: 43564
diff changeset
     6
  "~~/src/HOL/Library/RBT"
9d2e682a68eb tuned import
haftmann
parents: 43564
diff changeset
     7
  "~~/src/HOL/Library/Mapping"
51162
310b94ed1815 dropped now obsolete hint;
haftmann
parents: 48985
diff changeset
     8
  "~~/src/HOL/Library/IArray"
28213
b52f9205a02d New outline for codegen tutorial -- draft
haftmann
parents:
diff changeset
     9
begin
b52f9205a02d New outline for codegen tutorial -- draft
haftmann
parents:
diff changeset
    10
48951
b9238cbcdd41 more standard document preparation within session context;
wenzelm
parents: 48891
diff changeset
    11
ML_file "../antiquote_setup.ML"
b9238cbcdd41 more standard document preparation within session context;
wenzelm
parents: 48891
diff changeset
    12
ML_file "../more_antiquote.ML"
48891
c0eafbd55de3 prefer ML_file over old uses;
wenzelm
parents: 46517
diff changeset
    13
61143
5f898411ce87 eliminated \<Colon> from syntax of constraints;
wenzelm
parents: 59378
diff changeset
    14
no_syntax (output)
5f898411ce87 eliminated \<Colon> from syntax of constraints;
wenzelm
parents: 59378
diff changeset
    15
  "_constrain" :: "logic => type => logic"  ("_::_" [4, 0] 3)
5f898411ce87 eliminated \<Colon> from syntax of constraints;
wenzelm
parents: 59378
diff changeset
    16
  "_constrain" :: "prop' => type => prop'"  ("_::_" [4, 0] 3)
5f898411ce87 eliminated \<Colon> from syntax of constraints;
wenzelm
parents: 59378
diff changeset
    17
5f898411ce87 eliminated \<Colon> from syntax of constraints;
wenzelm
parents: 59378
diff changeset
    18
syntax (output)
5f898411ce87 eliminated \<Colon> from syntax of constraints;
wenzelm
parents: 59378
diff changeset
    19
  "_constrain" :: "logic => type => logic"  ("_ :: _" [4, 0] 3)
5f898411ce87 eliminated \<Colon> from syntax of constraints;
wenzelm
parents: 59378
diff changeset
    20
  "_constrain" :: "prop' => type => prop'"  ("_ :: _" [4, 0] 3)
38503
7115853eaf8a pretty constraint syntax; tuned theory imports
haftmann
parents: 38460
diff changeset
    21
59324
f5f9993a168d prefer option for default code printing width
haftmann
parents: 56240
diff changeset
    22
declare [[default_code_width = 74]]
34071
93bfbb557e2e default_code_width is now proper theory data
haftmann
parents: 32833
diff changeset
    23
42669
04dfffda5671 more conventional naming scheme: names_long, names_short, names_unique;
wenzelm
parents: 42358
diff changeset
    24
declare [[names_unique = false]]
28213
b52f9205a02d New outline for codegen tutorial -- draft
haftmann
parents:
diff changeset
    25
b52f9205a02d New outline for codegen tutorial -- draft
haftmann
parents:
diff changeset
    26
end