equal
deleted
inserted
replaced
43 use "thm.ML"; |
43 use "thm.ML"; |
44 use "display.ML"; |
44 use "display.ML"; |
45 use "fact_index.ML"; |
45 use "fact_index.ML"; |
46 use "pure_thy.ML"; |
46 use "pure_thy.ML"; |
47 use "drule.ML"; |
47 use "drule.ML"; |
48 use "meta_simplifier.ML"; |
|
49 use "tctical.ML"; |
48 use "tctical.ML"; |
50 use "search.ML"; |
49 use "search.ML"; |
|
50 use "meta_simplifier.ML"; |
51 use "tactic.ML"; |
51 use "tactic.ML"; |
52 |
52 |
53 (*proof term operations*) |
53 (*proof term operations*) |
54 cd "Proof"; use "ROOT.ML"; cd ".."; |
54 cd "Proof"; use "ROOT.ML"; cd ".."; |
55 |
55 |