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