changeset 9157 | 998dd2fb5795 |
parent 7576 | 594f09166c38 |
child 9888 | c5622848bf18 |
--- a/src/FOL/ROOT.ML Tue Jun 27 23:43:46 2000 +0200 +++ b/src/FOL/ROOT.ML Wed Jun 28 10:37:08 2000 +0200 @@ -16,6 +16,7 @@ use "~~/src/Provers/splitter.ML"; use "~~/src/Provers/ind.ML"; use "~~/src/Provers/hypsubst.ML"; +use "~~/src/Provers/make_elim.ML"; use "~~/src/Provers/classical.ML"; use "~~/src/Provers/blast.ML"; use "~~/src/Provers/clasimp.ML";