changeset 9888 | c5622848bf18 |
parent 9157 | 998dd2fb5795 |
child 11674 | c67d5ed31417 |
--- a/src/FOL/ROOT.ML Thu Sep 07 20:48:34 2000 +0200 +++ b/src/FOL/ROOT.ML Thu Sep 07 20:48:51 2000 +0200 @@ -16,6 +16,7 @@ use "~~/src/Provers/splitter.ML"; use "~~/src/Provers/ind.ML"; use "~~/src/Provers/hypsubst.ML"; +use "~~/src/Provers/rulify.ML"; use "~~/src/Provers/make_elim.ML"; use "~~/src/Provers/classical.ML"; use "~~/src/Provers/blast.ML";