src/HOL/Presburger.thy
changeset 28402 09e4aa3ddc25
parent 28290 4cc2b6046258
child 28967 3bdb1eae352c
--- a/src/HOL/Presburger.thy	Mon Sep 29 12:31:58 2008 +0200
+++ b/src/HOL/Presburger.thy	Mon Sep 29 12:31:59 2008 +0200
@@ -6,11 +6,10 @@
 header {* Decision Procedure for Presburger Arithmetic *}
 
 theory Presburger
-imports Arith_Tools SetInterval
+imports Groebner_Basis SetInterval
 uses
   "Tools/Qelim/cooper_data.ML"
   "Tools/Qelim/generated_cooper.ML"
-  "Tools/Qelim/qelim.ML"
   ("Tools/Qelim/cooper.ML")
   ("Tools/Qelim/presburger.ML")
 begin