| 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 |
| Sun, 22 Jul 2007 17:53:45 +0200 | chaieb | Added quantifier elimination in dense linear orders after Langford; locale dense_linear_order renamed to constr_dense_linear_order (since it requires the beween constant). locale dense_linear_order is now the classical definition of DLO. constr_dense_linear_order is an instance of dense_linear_order; Method dlo now applies the langford QE, odl Method dlo renamed to ferrack, since it ia a QE only in interpretations where between is interpreted in a manner to vanish after substitution. | changeset | files |
| Sun, 22 Jul 2007 17:53:42 +0200 | chaieb | Tunes Proof | changeset | files |