src/HOL/Dense_Linear_Order.thy
2008-02-04 chaieb 2008-02-04 replaced class by locale
2007-10-19 wenzelm 2007-10-19 tuned proofs;
2007-10-16 haftmann 2007-10-16 global class syntax
2007-10-08 haftmann 2007-10-08 added proper subclass concept; improved class target
2007-09-29 haftmann 2007-09-29 proper syntax during class specification
2007-09-23 wenzelm 2007-09-23 tuned ML setup;
2007-09-18 ballarin 2007-09-18 Simplified proofs due to transitivity reasoner setup.
2007-08-24 haftmann 2007-08-24 moved class dense_linear_order to Orderings.thy
2007-08-22 chaieb 2007-08-22 Axioms for class no longer use object-universal quantifiers
2007-08-20 haftmann 2007-08-20 turned locales intro classes
2007-08-14 wenzelm 2007-08-14 fixed dummyT (used as constraint);
2007-07-31 chaieb 2007-07-31 Tuned document
2007-07-22 wenzelm 2007-07-22 fixed document;
2007-07-22 chaieb 2007-07-22 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.
2007-06-21 huffman 2007-06-21 spelling
2007-06-21 wenzelm 2007-06-21 moved quantifier elimination tools to Tools/Qelim/;
2007-06-21 wenzelm 2007-06-21 Dense linear order witout endpoints and a quantifier elimination procedure in Ferrante and Rackoff style.