equal
deleted
inserted
replaced
53 use "ROOT.ML"; |
53 use "ROOT.ML"; |
54 cd ".."; |
54 cd ".."; |
55 |
55 |
56 use "install_pp.ML"; |
56 use "install_pp.ML"; |
57 |
57 |
|
58 val quick_and_dirty = ref false; |
|
59 |
58 (*several object-logics declare theories named List or Option, hiding |
60 (*several object-logics declare theories named List or Option, hiding |
59 the eponymous basis library structures*) |
61 the eponymous basis library structures*) |
60 structure BasisLibrary = |
62 structure BasisLibrary = |
61 struct |
63 struct |
62 structure List = List and Option = Option; |
64 structure List = List and Option = Option; |