equal
deleted
inserted
replaced
3 *) |
3 *) |
4 |
4 |
5 header {* Quatifier elimination for R(0,1,+,<) *} |
5 header {* Quatifier elimination for R(0,1,+,<) *} |
6 |
6 |
7 theory ReflectedFerrack |
7 theory ReflectedFerrack |
8 imports GCD Real Efficient_Nat |
8 imports Main GCD Real Efficient_Nat |
9 uses ("linreif.ML") ("linrtac.ML") |
9 uses ("linreif.ML") ("linrtac.ML") |
10 begin |
10 begin |
11 |
11 |
12 |
12 |
13 (*********************************************************************************) |
13 (*********************************************************************************) |
14 (* SOME GENERAL STUFF< HAS TO BE MOVED IN SOME LIB *) |
14 (* SOME GENERAL STUFF< HAS TO BE MOVED IN SOME LIB *) |