# HG changeset patch
# User wenzelm
# Date 880559087 -3600
# Node ID aa84d9c6245470fdb6eddd727adaa72e6f114184
# Parent  81132a38996a1100d4f1f9a2dabaee978e0d207c
added Arith provers;

diff -r 81132a38996a -r aa84d9c62454 src/HOL/ROOT.ML
--- a/src/HOL/ROOT.ML	Wed Nov 26 16:44:25 1997 +0100
+++ b/src/HOL/ROOT.ML	Wed Nov 26 16:44:47 1997 +0100
@@ -21,7 +21,9 @@
 use "$ISABELLE_HOME/src/Provers/hypsubst.ML";
 use "$ISABELLE_HOME/src/Provers/classical.ML";
 use "$ISABELLE_HOME/src/Provers/blast.ML";
-use "$ISABELLE_HOME/src/Provers/nat_transitive.ML";
+use "$ISABELLE_HOME/src/Provers/Arith/nat_transitive.ML";
+use "$ISABELLE_HOME/src/Provers/Arith/cancel_sums.ML";
+use "$ISABELLE_HOME/src/Provers/Arith/cancel_factor.ML";
 
 use "thy_data.ML";
 
@@ -37,6 +39,9 @@
 use_thy "Gfp";
 
 use "datatype.ML";
+use_thy "Arith";
+use "arith_data.ML";
+
 use "ind_syntax.ML";
 use "add_ind_def.ML";
 use_thy "intr_elim";