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