equal
deleted
inserted
replaced
1 (* Title: HOL/Reflection/MIR.thy |
1 (* Title: HOL/Reflection/MIR.thy |
2 Author: Amine Chaieb |
2 Author: Amine Chaieb |
3 *) |
3 *) |
4 |
4 |
5 theory MIR |
5 theory MIR |
6 imports Complex_Main Efficient_Nat |
6 imports Complex_Main Dense_Linear_Order Efficient_Nat |
7 uses ("mir_tac.ML") |
7 uses ("mir_tac.ML") |
8 begin |
8 begin |
9 |
9 |
10 section {* Quantifier elimination for @{text "\<real> (0, 1, +, floor, <)"} *} |
10 section {* Quantifier elimination for @{text "\<real> (0, 1, +, floor, <)"} *} |
11 |
11 |