isabelle: doc-src/Codegen/Thy/ROOT.ML@1886cddaf8a5 (annotated)

20948 9b9910b82645 initial draft haftmann parents: diff changeset	1
28419 f65e8b318581 re-canibalised manual haftmann parents: 28213 diff changeset	2	no_document use_thy "Setup";
28213 b52f9205a02d New outline for codegen tutorial -- draft haftmann parents: 21147 diff changeset	3
b52f9205a02d New outline for codegen tutorial -- draft haftmann parents: 21147 diff changeset	4	use_thy "Introduction";
38405 7935b334893e sketch of new outline haftmann parents: 37613 diff changeset	5	use_thy "Foundations";
7935b334893e sketch of new outline haftmann parents: 37613 diff changeset	6	use_thy "Refinement";
37613 355ec1b521e6 split off predicate compiler into separate theory haftmann parents: 31050 diff changeset	7	use_thy "Inductive_Predicate";
38510 ec0408c7328b stub for evaluation chapter haftmann parents: 38405 diff changeset	8	use_thy "Evaluation";
31050 555b56b66fcf adaptation replaces adaption haftmann parents: 30734 diff changeset	9	use_thy "Adaptation";
28213 b52f9205a02d New outline for codegen tutorial -- draft haftmann parents: 21147 diff changeset	10	use_thy "Further";