doc-src/IsarAdvanced/Codegen/Thy/Setup.thy
author wenzelm
Thu, 09 Oct 2008 20:53:24 +0200
changeset 28555 d59712ee942c
parent 28447 df77ed974a78
child 28593 f087237af65d
permissions -rw-r--r--
added enabled; removed pseudo-parallel version of profile -- CRITICAL prevents future join;
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
28419
f65e8b318581 re-canibalised manual
haftmann
parents: 28213
diff changeset
     2
imports Complex_Main
28440
0b9ddfa6458e added more_antiquote.ML
haftmann
parents: 28428
diff changeset
     3
uses "../../../antiquote_setup.ML" "../../../more_antiquote.ML"
28213
b52f9205a02d New outline for codegen tutorial -- draft
haftmann
parents:
diff changeset
     4
begin
b52f9205a02d New outline for codegen tutorial -- draft
haftmann
parents:
diff changeset
     5
28447
haftmann
parents: 28440
diff changeset
     6
ML {* no_document use_thys
haftmann
parents: 28440
diff changeset
     7
  ["Efficient_Nat", "Code_Char_chr", "Product_ord"] *}
28419
f65e8b318581 re-canibalised manual
haftmann
parents: 28213
diff changeset
     8
28213
b52f9205a02d New outline for codegen tutorial -- draft
haftmann
parents:
diff changeset
     9
ML_val {* Code_Target.code_width := 74 *}
b52f9205a02d New outline for codegen tutorial -- draft
haftmann
parents:
diff changeset
    10
b52f9205a02d New outline for codegen tutorial -- draft
haftmann
parents:
diff changeset
    11
end