src/HOL/IsaMakefile
changeset 5605 e86700ddc7d4
parent 5564 f16de69b7c0c
child 5616 497eeeace3fc
--- a/src/HOL/IsaMakefile	Fri Oct 02 10:41:35 1998 +0200
+++ b/src/HOL/IsaMakefile	Fri Oct 02 10:42:37 1998 +0200
@@ -30,7 +30,8 @@
 	@cd $(SRC)/Pure; $(ISATOOL) make Pure
 
 $(OUT)/HOL: $(OUT)/Pure $(SRC)/Provers/Arith/cancel_sums.ML \
-  $(SRC)/Provers/Arith/nat_transitive.ML $(SRC)/Provers/blast.ML \
+  $(SRC)/Provers/Arith/nat_transitive.ML \
+  $(SRC)/Provers/Arith/abel_cancel.ML $(SRC)/Provers/blast.ML \
   $(SRC)/Provers/clasimp.ML $(SRC)/Provers/classical.ML \
   $(SRC)/Provers/hypsubst.ML $(SRC)/Provers/simplifier.ML \
   $(SRC)/Provers/splitter.ML $(SRC)/Pure/section_utils.ML \
@@ -133,6 +134,7 @@
   Real/Lubs.ML Real/Lubs.thy Real/PNat.ML Real/PNat.thy \
   Real/PRat.ML Real/PRat.thy Real/PReal.ML Real/PReal.thy \
   Real/RComplete.ML Real/RComplete.thy Real/Real.ML Real/Real.thy \
+  Real/RealDef.ML Real/RealDef.thy Real/simproc.ML \
   Real/RealAbs.ML Real/RealAbs.thy Real/ROOT.ML
 	@$(ISATOOL) usedir $(OUT)/HOL Real