# HG changeset patch
# User haftmann
# Date 1273496224 -7200
# Node ID 2cad8904c4ff0a863825f442505301736c4af15e
# Parent  5f9fe7b3295d749bd6faee8a4cd8739e9786a643
updated references to ML files

diff -r 5f9fe7b3295d -r 2cad8904c4ff src/HOL/IsaMakefile
--- a/src/HOL/IsaMakefile	Mon May 10 14:55:06 2010 +0200
+++ b/src/HOL/IsaMakefile	Mon May 10 14:57:04 2010 +0200
@@ -303,8 +303,7 @@
   Tools/Predicate_Compile/predicate_compile_pred.ML \
   Tools/quickcheck_generators.ML \
   Tools/Qelim/cooper.ML \
-  Tools/Qelim/generated_cooper.ML \
-  Tools/Qelim/presburger.ML \
+  Tools/Qelim/cooper_procedure.ML \
   Tools/Qelim/qelim.ML \
   Tools/Quotient/quotient_def.ML \
   Tools/Quotient/quotient_info.ML \
diff -r 5f9fe7b3295d -r 2cad8904c4ff src/HOL/Presburger.thy
--- a/src/HOL/Presburger.thy	Mon May 10 14:55:06 2010 +0200
+++ b/src/HOL/Presburger.thy	Mon May 10 14:57:04 2010 +0200
@@ -10,7 +10,6 @@
   "Tools/Qelim/qelim.ML"
   "Tools/Qelim/cooper_procedure.ML"
   ("Tools/Qelim/cooper.ML")
-  ("Tools/Qelim/presburger.ML")
 begin
 
 subsection{* The @{text "-\<infinity>"} and @{text "+\<infinity>"} Properties *}