equal
deleted
inserted
replaced
7 *) |
7 *) |
8 |
8 |
9 header {* Presburger Arithmetic: Cooper's Algorithm *} |
9 header {* Presburger Arithmetic: Cooper's Algorithm *} |
10 |
10 |
11 theory Presburger |
11 theory Presburger |
12 imports "Integ/NatSimprocs" SetInterval |
12 imports NatSimprocs SetInterval |
13 uses |
13 uses |
14 ("Tools/Presburger/cooper_dec.ML") |
14 ("Tools/Presburger/cooper_dec.ML") |
15 ("Tools/Presburger/cooper_proof.ML") |
15 ("Tools/Presburger/cooper_proof.ML") |
16 ("Tools/Presburger/qelim.ML") |
16 ("Tools/Presburger/qelim.ML") |
17 ("Tools/Presburger/reflected_presburger.ML") |
17 ("Tools/Presburger/reflected_presburger.ML") |