| Sun, 22 Jul 2007 21:20:55 +0200 | wenzelm | added simultaneous use_thys; | changeset | files |
| Sun, 22 Jul 2007 21:20:54 +0200 | wenzelm | avoid polymorphic equality; | changeset | files |
| 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 |
| Sun, 22 Jul 2007 17:53:51 +0200 | chaieb | Tuned proof : dlo replaced by ferrack | changeset | files |
| Sun, 22 Jul 2007 17:53:50 +0200 | chaieb | tuned | changeset | files |
| Sun, 22 Jul 2007 17:53:48 +0200 | chaieb | Renamed attribute dlo into attribute ferrack | changeset | files |