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