changeset 24584 | 01e83ffa6c54 |
parent 24020 | ed4d7abffee7 |
child 25979 | 3297781f8141 |
24583:d77e4d48e497 | 24584:01e83ffa6c54 |
---|---|
1 (* Title: HOL/Tools/ferrante_rackoff_data.ML |
1 (* Title: HOL/Tools/Qelim/ferrante_rackoff_data.ML |
2 ID: $Id$ |
2 ID: $Id$ |
3 Author: Amine Chaieb, TU Muenchen |
3 Author: Amine Chaieb, TU Muenchen |
4 |
4 |
5 Context data for Ferrante and Rackoff's algorithm for quantifier |
5 Context data for Ferrante and Rackoff's algorithm for quantifier |
6 elimination in dense linear orders. |
6 elimination in dense linear orders. |