doc-src/Codegen/Thy/ROOT.ML
author immler@in.tum.de
Sat, 14 Mar 2009 15:45:45 +0100
changeset 30535 db8b10fd51a4
parent 30226 2f4684e2ea95
child 30734 ab05be086c4a
permissions -rw-r--r--
show certain errors to the user
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
20948
9b9910b82645 initial draft
haftmann
parents:
diff changeset
     1
9b9910b82645 initial draft
haftmann
parents:
diff changeset
     2
(* $Id$ *)
9b9910b82645 initial draft
haftmann
parents:
diff changeset
     3
28419
f65e8b318581 re-canibalised manual
haftmann
parents: 28213
diff changeset
     4
no_document use_thy "Setup";
28420
293b166c45c5 fixed slips
haftmann
parents: 28419
diff changeset
     5
no_document use_thys ["Efficient_Nat"];
28213
b52f9205a02d New outline for codegen tutorial -- draft
haftmann
parents: 21147
diff changeset
     6
b52f9205a02d New outline for codegen tutorial -- draft
haftmann
parents: 21147
diff changeset
     7
use_thy "Introduction";
b52f9205a02d New outline for codegen tutorial -- draft
haftmann
parents: 21147
diff changeset
     8
use_thy "Program";
b52f9205a02d New outline for codegen tutorial -- draft
haftmann
parents: 21147
diff changeset
     9
use_thy "Adaption";
b52f9205a02d New outline for codegen tutorial -- draft
haftmann
parents: 21147
diff changeset
    10
use_thy "Further";
28419
f65e8b318581 re-canibalised manual
haftmann
parents: 28213
diff changeset
    11
use_thy "ML";