# HG changeset patch
# User paulson
# Date 907317757 -7200
# Node ID e86700ddc7d4d2a79e5e43539fdc1f2dbbd19796
# Parent  cd17004d09e1adebe40ca2513bc060fd0af41fe7
new files Provers/Arith/abel_cancel.ML and Real/simproc.ML

diff -r cd17004d09e1 -r e86700ddc7d4 src/HOL/IsaMakefile
--- 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