changeset 4962 | e9217cb15b42 |
parent 4949 | c73f72daee64 |
child 4978 | f14ec8ec1db1 |
4961:27f559b54c57 | 4962:e9217cb15b42 |
---|---|
47 use "tactic.ML"; |
47 use "tactic.ML"; |
48 use "goals.ML"; |
48 use "goals.ML"; |
49 use "axclass.ML"; |
49 use "axclass.ML"; |
50 |
50 |
51 (*theory parser and loader*) |
51 (*theory parser and loader*) |
52 val global_names = ref false; (* FIXME tmp *) |
|
53 cd "Thy"; |
52 cd "Thy"; |
54 use "ROOT.ML"; |
53 use "ROOT.ML"; |
55 cd ".."; |
54 cd ".."; |
56 |
55 |
57 use "install_pp.ML"; |
56 use "install_pp.ML"; |