isabelle: doc-src/Codegen/Thy/ROOT.ML@581c1e5f53e0 (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";
28420 293b166c45c5 fixed slips haftmann parents: 28419 diff changeset	3	no_document use_thys ["Efficient_Nat"];
28213 b52f9205a02d New outline for codegen tutorial -- draft haftmann parents: 21147 diff changeset	4
b52f9205a02d New outline for codegen tutorial -- draft haftmann parents: 21147 diff changeset	5	use_thy "Introduction";
b52f9205a02d New outline for codegen tutorial -- draft haftmann parents: 21147 diff changeset	6	use_thy "Program";
37613 355ec1b521e6 split off predicate compiler into separate theory haftmann parents: 31050 diff changeset	7	use_thy "Inductive_Predicate";
31050 555b56b66fcf adaptation replaces adaption haftmann parents: 30734 diff changeset	8	use_thy "Adaptation";
28213 b52f9205a02d New outline for codegen tutorial -- draft haftmann parents: 21147 diff changeset	9	use_thy "Further";
28419 f65e8b318581 re-canibalised manual haftmann parents: 28213 diff changeset	10	use_thy "ML";