equal
deleted
inserted
replaced
51 use "General/balanced_tree.ML"; |
51 use "General/balanced_tree.ML"; |
52 use "General/graph.ML"; |
52 use "General/graph.ML"; |
53 use "General/linear_set.ML"; |
53 use "General/linear_set.ML"; |
54 use "General/buffer.ML"; |
54 use "General/buffer.ML"; |
55 use "General/xml.ML"; |
55 use "General/xml.ML"; |
56 use "General/xml_data.ML"; |
|
57 use "General/pretty.ML"; |
56 use "General/pretty.ML"; |
58 use "General/path.ML"; |
57 use "General/path.ML"; |
59 use "General/url.ML"; |
58 use "General/url.ML"; |
60 use "General/file.ML"; |
59 use "General/file.ML"; |
61 use "General/yxml.ML"; |
60 use "General/yxml.ML"; |