Sun, 22 Jul 2007 21:20:53 +0200 | wenzelm | blast_hyp_subst_tac: plain bool argument; | changeset | files |
Sun, 22 Jul 2007 17:53:55 +0200 | chaieb | Context data for QE in DLO (Langford's algorithm) | changeset | files |
Sun, 22 Jul 2007 17:53:54 +0200 | chaieb | Quantifier elimination for Dense linear orders after Langford | changeset | files |