| changeset 37744 | 3daaf23b9ab4 |
| parent 37120 | 5df087c6ce94 |
| child 38549 | d0385f2764d8 |
| 37743:0a3fa8fbcdc5 | 37744:3daaf23b9ab4 |
|---|---|
1 (* Title: HOL/Tools/Qelim/ferrante_rackoff.ML |
1 (* Title: HOL/Decision_Procs/ferrante_rackoff.ML |
2 Author: Amine Chaieb, TU Muenchen |
2 Author: Amine Chaieb, TU Muenchen |
3 |
3 |
4 Ferrante and Rackoff's algorithm for quantifier elimination in dense |
4 Ferrante and Rackoff's algorithm for quantifier elimination in dense |
5 linear orders. Proof-synthesis and tactic. |
5 linear orders. Proof-synthesis and tactic. |
6 *) |
6 *) |