equal
deleted
inserted
replaced
5 header {* Decision Procedure for Presburger Arithmetic *} |
5 header {* Decision Procedure for Presburger Arithmetic *} |
6 |
6 |
7 theory Presburger |
7 theory Presburger |
8 imports Groebner_Basis SetInterval |
8 imports Groebner_Basis SetInterval |
9 uses |
9 uses |
|
10 "Tools/Qelim/qelim.ML" |
10 "Tools/Qelim/cooper_data.ML" |
11 "Tools/Qelim/cooper_data.ML" |
11 "Tools/Qelim/generated_cooper.ML" |
12 "Tools/Qelim/generated_cooper.ML" |
12 ("Tools/Qelim/cooper.ML") |
13 ("Tools/Qelim/cooper.ML") |
13 ("Tools/Qelim/presburger.ML") |
14 ("Tools/Qelim/presburger.ML") |
14 begin |
15 begin |