src/HOL/Decision_Procs/Parametric_Ferrante_Rackoff.thy
2010-04-26 haftmann 2010-04-26 use new classes (linordered_)field_inverse_zero
2010-04-26 haftmann 2010-04-26 dropped group_simps, ring_simps, field_eq_simps; classes division_ring_inverse_zero, field_inverse_zero, linordered_field_inverse_zero
2010-03-07 wenzelm 2010-03-07 modernized structure Object_Logic;
2010-03-01 haftmann 2010-03-01 replaced a couple of constsdefs by definitions (also some old primrecs by modern ones)
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 using code antiquotation
2010-02-08 haftmann 2010-02-08 tuned proof
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-11-12 hoelzl 2009-11-12 New list theorems; added map_map to simpset, this is the prefered direction; allow sorting by a key
2009-10-28 wenzelm 2009-10-28 eliminated hard tabulators, guessing at each author's individual tab-width;
2009-10-26 wenzelm 2009-10-26 tuned;
2009-10-25 chaieb 2009-10-25 Add a quantifier elimination for parametric linear arithmetic over ordered fields (parameters are multivariate polynomials)