moved import of module qelim to theory Presburger
authorhaftmann
Sun, 22 Mar 2009 20:46:12 +0100
changeset 30656 ddb1fafa2dcb
parent 30655 88131f2807b6
child 30657 db260dfd2d8c
moved import of module qelim to theory Presburger
src/HOL/Presburger.thy
--- a/src/HOL/Presburger.thy	Sun Mar 22 20:46:11 2009 +0100
+++ b/src/HOL/Presburger.thy	Sun Mar 22 20:46:12 2009 +0100
@@ -7,6 +7,7 @@
 theory Presburger
 imports Groebner_Basis SetInterval
 uses
+  "Tools/Qelim/qelim.ML"
   "Tools/Qelim/cooper_data.ML"
   "Tools/Qelim/generated_cooper.ML"
   ("Tools/Qelim/cooper.ML")