equal
deleted
inserted
replaced
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"; |
55 ML_file "General/stack.ML"; |
56 ML_file "General/stack.ML"; |
56 ML_file "General/queue.ML"; |
57 ML_file "General/queue.ML"; |
57 ML_file "General/heap.ML"; |
58 ML_file "General/heap.ML"; |
58 ML_file "General/same.ML"; |
59 ML_file "General/same.ML"; |
59 ML_file "General/ord_list.ML"; |
60 ML_file "General/ord_list.ML"; |