# HG changeset patch
# User chaieb
# Date 1204119590 -3600
# Node ID 420c1947511cfe10f7a0f5ae9597f974ba9e2763
# Parent  7c265e3da23cbc2809e707cdd5fb81647187d154
loads Tools/Qelim/qelim.ML

diff -r 7c265e3da23c -r 420c1947511c src/HOL/Presburger.thy
--- a/src/HOL/Presburger.thy	Wed Feb 27 14:39:49 2008 +0100
+++ b/src/HOL/Presburger.thy	Wed Feb 27 14:39:50 2008 +0100
@@ -10,6 +10,7 @@
 uses
   "Tools/Qelim/cooper_data.ML"
   "Tools/Qelim/generated_cooper.ML"
+  "Tools/Qelim/qelim.ML"
   ("Tools/Qelim/cooper.ML")
   ("Tools/Qelim/presburger.ML")
 begin