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