changeset 24584 | 01e83ffa6c54 |
parent 23567 | 28c6a0118818 |
child 30304 | d8e4cd2ac2a1 |
24583:d77e4d48e497 | 24584:01e83ffa6c54 |
---|---|
1 (* Title: HOL/Tools/ferrante_rackoff.ML |
1 (* Title: HOL/Tools/Qelim/ferrante_rackoff.ML |
2 ID: $Id$ |
2 ID: $Id$ |
3 Author: Amine Chaieb, TU Muenchen |
3 Author: Amine Chaieb, TU Muenchen |
4 |
4 |
5 Ferrante and Rackoff's algorithm for quantifier elimination in dense |
5 Ferrante and Rackoff's algorithm for quantifier elimination in dense |
6 linear orders. Proof-synthesis and tactic. |
6 linear orders. Proof-synthesis and tactic. |