src/HOL/Dense_Linear_Order.thy
Tue, 14 Aug 2007 23:22:49 +0200 wenzelm fixed dummyT (used as constraint);
Tue, 31 Jul 2007 09:31:19 +0200 chaieb Tuned document
Sun, 22 Jul 2007 23:23:39 +0200 wenzelm fixed document;
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.
Thu, 21 Jun 2007 23:28:44 +0200 huffman spelling
Thu, 21 Jun 2007 20:48:48 +0200 wenzelm moved quantifier elimination tools to Tools/Qelim/;
Thu, 21 Jun 2007 15:42:06 +0200 wenzelm Dense linear order witout endpoints
less more (0) tip