--- 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
--- 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$