# HG changeset patch
# User wenzelm
# Date 968352611 -7200
# Node ID 133c845d2bd1ac90925f8246579a372d530e6625
# Parent  144ecc001b8f1e8eb2b196173a6d9eaba98367e0
added Provers/rulify;

diff -r 144ecc001b8f -r 133c845d2bd1 src/HOL/ROOT.ML
--- a/src/HOL/ROOT.ML	Thu Sep 07 20:49:39 2000 +0200
+++ b/src/HOL/ROOT.ML	Thu Sep 07 20:50:11 2000 +0200
@@ -20,6 +20,7 @@
 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/make_elim.ML";
 use "~~/src/Provers/classical.ML";
 use "~~/src/Provers/blast.ML";