Wed, 31 Dec 2008 00:08:13 +0100 | wenzelm | moved old add_term_vars, add_term_frees etc. to structure OldTerm; | file | diff | annotate |
Tue, 31 Jul 2007 09:31:26 +0200 | chaieb | find_body goes under meta-quantifier ; tactic generalizes free variables; | file | diff | annotate |
Sun, 22 Jul 2007 17:53:54 +0200 | chaieb | Quantifier elimination for Dense linear orders after Langford | file | diff | annotate |