equal
deleted
inserted
replaced
2 Author: Amine Chaieb |
2 Author: Amine Chaieb |
3 *) |
3 *) |
4 |
4 |
5 theory MIR |
5 theory MIR |
6 imports Complex_Main Dense_Linear_Order DP_Library |
6 imports Complex_Main Dense_Linear_Order DP_Library |
7 "~~/src/HOL/Library/Code_Target_Numeral" "~~/src/HOL/Library/Old_Recdef" |
7 "HOL-Library.Code_Target_Numeral" "HOL-Library.Old_Recdef" |
8 begin |
8 begin |
9 |
9 |
10 section \<open>Quantifier elimination for \<open>\<real> (0, 1, +, floor, <)\<close>\<close> |
10 section \<open>Quantifier elimination for \<open>\<real> (0, 1, +, floor, <)\<close>\<close> |
11 |
11 |
12 declare of_int_floor_cancel [simp del] |
12 declare of_int_floor_cancel [simp del] |