2008-07-18 haftmann 2008-07-18 moved op dvd to theory Ring_and_Field; generalized a couple of lemmas
2008-02-17 huffman 2008-02-17 New simpler representation of numerals, using Bit0 and Bit1 instead of BIT, B0, and B1
2007-11-28 haftmann 2007-11-28 dropped legacy ml bindings
2007-08-21 nipkow 2007-08-21 Added mod cancellation simproc
2007-07-24 nipkow 2007-07-24 Added cancel simprocs for dvd on nat and int
2007-07-20 haftmann 2007-07-20 moved class ord from Orderings.thy to HOL.thy
2007-06-17 nipkow 2007-06-17 tuned laws for cancellation in divisions for fields.
2007-06-16 nipkow 2007-06-16 tuned
2007-06-16 nipkow 2007-06-16 The simprocs "divide_cancel_factor" and "ring_eq_cancel_factor" no longer need class numeral_ring. This made a number of special simp-thms redundant.
2007-06-15 nipkow 2007-06-15 made divide_self a simp rule
2007-05-31 wenzelm 2007-05-31 moved Integ files to canonical place;