50 section "Bootstrap phase 2: towards ML within Isar context"; |
50 section "Bootstrap phase 2: towards ML within Isar context"; |
51 |
51 |
52 subsection "Library of general tools"; |
52 subsection "Library of general tools"; |
53 |
53 |
54 ML_file "General/integer.ML"; |
54 ML_file "General/integer.ML"; |
55 ML_file "General/rat.ML"; |
|
56 ML_file "General/stack.ML"; |
55 ML_file "General/stack.ML"; |
57 ML_file "General/queue.ML"; |
56 ML_file "General/queue.ML"; |
58 ML_file "General/heap.ML"; |
57 ML_file "General/heap.ML"; |
59 ML_file "General/same.ML"; |
58 ML_file "General/same.ML"; |
60 ML_file "General/ord_list.ML"; |
59 ML_file "General/ord_list.ML"; |
61 ML_file "General/balanced_tree.ML"; |
60 ML_file "General/balanced_tree.ML"; |
62 ML_file "General/linear_set.ML"; |
61 ML_file "General/linear_set.ML"; |
63 ML_file "General/buffer.ML"; |
62 ML_file "General/buffer.ML"; |
64 ML_file "General/pretty.ML"; |
63 ML_file "General/pretty.ML"; |
|
64 ML_file "General/rat.ML"; |
65 ML_file "PIDE/xml.ML"; |
65 ML_file "PIDE/xml.ML"; |
66 ML_file "General/path.ML"; |
66 ML_file "General/path.ML"; |
67 ML_file "General/url.ML"; |
67 ML_file "General/url.ML"; |
68 ML_file "General/file.ML"; |
68 ML_file "General/file.ML"; |
69 ML_file "General/long_name.ML"; |
69 ML_file "General/long_name.ML"; |