equal
deleted
inserted
replaced
7 method to eliminate on \<exists>. *) |
7 method to eliminate on \<exists>. *) |
8 |
8 |
9 header {* Quantifier elimination for Presburger arithmetic *} |
9 header {* Quantifier elimination for Presburger arithmetic *} |
10 |
10 |
11 theory Reflected_Presburger |
11 theory Reflected_Presburger |
12 imports Main |
12 imports Main GCD |
13 begin |
13 begin |
14 |
14 |
15 (* Shadow syntax for integer terms *) |
15 (* Shadow syntax for integer terms *) |
16 datatype intterm = |
16 datatype intterm = |
17 Cst int |
17 Cst int |