changeset 47317 | 432b29a96f61 |
parent 47165 | 9344891b504b |
child 47432 | e1576d13e933 |
--- a/src/HOL/Presburger.thy Tue Apr 03 14:09:37 2012 +0200 +++ b/src/HOL/Presburger.thy Tue Apr 03 15:15:00 2012 +0200 @@ -5,7 +5,7 @@ header {* Decision Procedure for Presburger Arithmetic *} theory Presburger -imports Groebner_Basis SetInterval +imports Groebner_Basis Set_Interval uses "Tools/Qelim/qelim.ML" "Tools/Qelim/cooper_procedure.ML"