# HG changeset patch
# User wenzelm
# Date 880558885 -3600
# Node ID 5c1bfefd39b76a39367d6557d38ea9fe8819b03e
# Parent  3f5e8c4aa84d20f0284df8e8b88f820052bf317f
tuned;

diff -r 3f5e8c4aa84d -r 5c1bfefd39b7 src/HOL/IsaMakefile
--- a/src/HOL/IsaMakefile	Wed Nov 26 16:38:04 1997 +0100
+++ b/src/HOL/IsaMakefile	Wed Nov 26 16:41:25 1997 +0100
@@ -13,17 +13,17 @@
 	Divides Power Sexp Univ List RelPow Option Map
 
 PROVERS = hypsubst.ML classical.ML blast.ML \
-	simplifier.ML splitter.ML nat_transitive.ML 
+	simplifier.ML splitter.ML Arith/nat_transitive.ML Arith/cancel_sums.ML
 
 TFL   = dcterm.sml post.sml rules.new.sml rules.sig \
 	sys.sml tfl.sig tfl.sml thms.sig thms.sml thry.sig thry.sml   \
 	usyntax.sig usyntax.sml utils.sig utils.sml
 
 FILES = ROOT.ML add_ind_def.ML datatype.ML hologic.ML \
-	ind_syntax.ML cladata.ML simpdata.ML \
-	typedef.ML thy_syntax.ML thy_data.ML ../Pure/section_utils.ML \
+	ind_syntax.ML cladata.ML simpdata.ML arith_data.ML \
+	typedef.ML thy_syntax.ML thy_data.ML $(ISABELLE_HOME)/src/Pure/section_utils.ML \
 	$(NAMES:%=%.thy) $(NAMES:%=%.ML) $(TFL:%=../TFL/%) \
-	$(PROVERS:%=../Provers/%)
+	$(PROVERS:%=$(ISABELLE_HOME)/src/Provers/%)
 
 $(OUT)/HOL: $(OUT)/Pure $(FILES)
 	@$(ISATOOL) usedir -b $(OUT)/Pure HOL
diff -r 3f5e8c4aa84d -r 5c1bfefd39b7 src/Provers/README
--- a/src/Provers/README	Wed Nov 26 16:38:04 1997 +0100
+++ b/src/Provers/README	Wed Nov 26 16:41:25 1997 +0100
@@ -1,17 +1,23 @@
-			Provers
+
+                        Provers
 
 This directory contains ML sources of generic theorem proving tools.
 Typically, they can be applied to various logics, provided rules of a
 certain form are derivable.  Some of these are documented in the
 Reference Manual.
 
-blast.ML          -- generic tableau prover with proof reconstruction
-classical.ML      -- theorem prover for classical logics
-genelim.ML        -- bits and pieces for deriving elimination rules
-hypsubst.ML       -- tactic to substitute in the hypotheses
-ind.ML            -- a simple induction package
-nat_transitive.ML -- simple package for inequalities over nat
-simp.ML           -- powerful but slow simplifier
-simplifier.ML     -- fast simplifier
-splitter.ML       -- performs case splits for simplifier.ML
-typedsimp.ML      -- basic simplifier for explicitly typed logics
+blast.ML                -- generic tableau prover with proof reconstruction
+classical.ML            -- theorem prover for classical logics
+genelim.ML              -- bits and pieces for deriving elimination rules
+hypsubst.ML             -- tactic to substitute in the hypotheses
+ind.ML                  -- a simple induction package
+simp.ML                 -- powerful but slow simplifier
+simplifier.ML           -- fast simplifier
+splitter.ML             -- performs case splits for simplifier.ML
+typedsimp.ML            -- basic simplifier for explicitly typed logics
+
+directory Arith:
+  nat_transitive.ML     -- simple package for inequalities over nat
+
+
+$Id$