changeset 11770 | b6bb7a853dd2 |
parent 11685 | c786d9ce558e |
child 11837 | b2a9853ec6dd |
--- a/src/HOL/ROOT.ML Sun Oct 14 22:07:01 2001 +0200 +++ b/src/HOL/ROOT.ML Sun Oct 14 22:08:29 2001 +0200 @@ -20,7 +20,6 @@ use "~~/src/Provers/split_paired_all.ML"; use "~~/src/Provers/splitter.ML"; use "~~/src/Provers/hypsubst.ML"; -use "~~/src/Provers/rulify.ML"; use "~~/src/Provers/induct_method.ML"; use "~~/src/Provers/make_elim.ML"; use "~~/src/Provers/classical.ML";