equal
deleted
inserted
replaced
3 *) |
3 *) |
4 |
4 |
5 header {* Quatifier elimination for R(0,1,+,floor,<) *} |
5 header {* Quatifier elimination for R(0,1,+,floor,<) *} |
6 |
6 |
7 theory MIR |
7 theory MIR |
8 imports Real GCD Code_Integer |
8 imports List Real Code_Integer |
9 uses ("mireif.ML") ("mirtac.ML") |
9 uses ("mireif.ML") ("mirtac.ML") |
10 begin |
10 begin |
11 |
11 |
12 declare real_of_int_floor_cancel [simp del] |
12 declare real_of_int_floor_cancel [simp del] |
13 |
13 |
14 primrec alluopairs:: "'a list \<Rightarrow> ('a \<times> 'a) list" where |
14 primrec alluopairs:: "'a list \<Rightarrow> ('a \<times> 'a) list" where |
15 "alluopairs [] = []" |
15 "alluopairs [] = []" |