src/HOL/Decision_Procs/Dense_Linear_Order.thy
2010-03-18 blanchet 2010-03-18 now use "Named_Thms" for "noatp", and renamed "noatp" to "no_atp"
2010-02-19 haftmann 2010-02-19 moved remaning class operations from Algebras.thy to Groups.thy
2010-02-10 haftmann 2010-02-10 moved less_eq, less to Orderings.thy; moved abs, sgn to Groups.thy
2010-02-10 haftmann 2010-02-10 moved constants inverse and divide to Ring.thy
2010-02-08 haftmann 2010-02-08 dropped accidental duplication of "lin" prefix from cs. 108662d50512
2010-02-05 haftmann 2010-02-05 more consistent naming of type classes involving orderings (and lattices) -- c.f. NEWS
2010-01-28 haftmann 2010-01-28 new theory Algebras.thy for generic algebraic structures
2009-07-23 wenzelm 2009-07-23 renamed simpset_of to global_simpset_of, and local_simpset_of to simpset_of -- same for claset and clasimpset;
2009-04-29 haftmann 2009-04-29 farewell to class recpower
2009-04-05 chaieb 2009-04-05 fixed usage of rational constants
2009-03-27 haftmann 2009-03-27 merged
2009-03-27 haftmann 2009-03-27 normalized imports
2009-03-26 wenzelm 2009-03-26 interpretation/interpret: prefixes are mandatory by default;
2009-03-22 haftmann 2009-03-22 distributed contents of theory Arith_Tools to theories Int, IntDiv and NatBin accordingly
2009-03-16 wenzelm 2009-03-16 simplified method setup;
2009-03-13 wenzelm 2009-03-13 unified type Proof.method and pervasive METHOD combinators;
2009-03-11 hoelzl 2009-03-11 Updated paths in Decision_Procs comments and NEWS
2009-02-09 chaieb 2009-02-09 A generic decision procedure for linear rea arithmetic and normed vector spaces
2009-02-06 haftmann 2009-02-06 session Reflecion renamed to Decision_Procs, moved Dense_Linear_Order there