| Tue, 31 Jul 2007 09:31:19 +0200 | chaieb | Tuned document | file | diff | annotate |
| Sun, 22 Jul 2007 23:23:39 +0200 | wenzelm | fixed document; | file | diff | annotate |
| 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. | file | diff | annotate |
| Thu, 21 Jun 2007 23:28:44 +0200 | huffman | spelling | file | diff | annotate |
| Thu, 21 Jun 2007 20:48:48 +0200 | wenzelm | moved quantifier elimination tools to Tools/Qelim/; | file | diff | annotate |
| Thu, 21 Jun 2007 15:42:06 +0200 | wenzelm | Dense linear order witout endpoints | file | diff | annotate |