# HG changeset patch
# User haftmann
# Date 1179072921 -7200
# Node ID 9793d28d49ad7981a2725274f5d5168ed8dc6f78
# Parent  2863582c61b5f521626d4b8456d7ecbc96b1d7ef
added modules rat.ML and int.ML

diff -r 2863582c61b5 -r 9793d28d49ad src/HOL/IsaMakefile
--- a/src/HOL/IsaMakefile	Sun May 13 09:23:27 2007 +0200
+++ b/src/HOL/IsaMakefile	Sun May 13 18:15:21 2007 +0200
@@ -62,7 +62,8 @@
 Pure:
 	@cd $(SRC)/Pure; $(ISATOOL) make Pure
 
-$(OUT)/HOL: $(OUT)/Pure $(SRC)/Provers/Arith/abel_cancel.ML			\
+$(OUT)/HOL: $(OUT)/Pure $(SRC)/Pure/General/int.ML $(SRC)/Pure/General/rat.ML   \
+  $(SRC)/Provers/Arith/abel_cancel.ML			                        \
   $(SRC)/Provers/Arith/assoc_fold.ML						\
   $(SRC)/Provers/Arith/cancel_div_mod.ML					\
   $(SRC)/Provers/Arith/cancel_numeral_factor.ML					\
diff -r 2863582c61b5 -r 9793d28d49ad src/HOL/ROOT.ML
--- a/src/HOL/ROOT.ML	Sun May 13 09:23:27 2007 +0200
+++ b/src/HOL/ROOT.ML	Sun May 13 18:15:21 2007 +0200
@@ -22,6 +22,8 @@
 use "~~/src/Provers/classical.ML";
 use "~~/src/Provers/blast.ML";
 use "~~/src/Provers/clasimp.ML";
+use "~~/src/Pure/General/int.ML";
+use "~~/src/Pure/General/rat.ML";
 use "~~/src/Provers/Arith/fast_lin_arith.ML";
 use "~~/src/Provers/Arith/cancel_sums.ML";
 use "~~/src/Provers/Arith/assoc_fold.ML";