src/HOL/ROOT.ML
changeset 11837 b2a9853ec6dd
parent 11770 b6bb7a853dd2
child 11868 56db9f3a6b3e
--- a/src/HOL/ROOT.ML	Fri Oct 19 21:59:33 2001 +0200
+++ b/src/HOL/ROOT.ML	Fri Oct 19 22:00:08 2001 +0200
@@ -17,7 +17,6 @@
 use "hologic.ML";
 
 use "~~/src/Provers/simplifier.ML";
-use "~~/src/Provers/split_paired_all.ML";
 use "~~/src/Provers/splitter.ML";
 use "~~/src/Provers/hypsubst.ML";
 use "~~/src/Provers/induct_method.ML";