src/HOL/Ring_and_Field.thy
2009-11-13 nipkow 2009-11-13 moved lemma from Algebra/IntRing to Ring_and_Field
2009-10-30 haftmann 2009-10-30 tuned code setup
2009-10-29 haftmann 2009-10-29 moved algebraic classes to Ring_and_Field
2009-10-17 wenzelm 2009-10-17 eliminated hard tabulators, guessing at each author's individual tab-width; tuned headers;
2009-04-22 haftmann 2009-04-22 more localisation
2009-03-23 huffman 2009-03-23 clean up proofs of sign rules for multiplication; add list of lemmas mult_sign_intros
2009-03-22 nipkow 2009-03-22 merged
2009-03-22 nipkow 2009-03-22 1. New cancellation simprocs for common factors in inequations 2. Updated the documentation
2009-03-21 huffman 2009-03-21 move field lemmas into class locale context
2009-03-04 blanchet 2009-03-04 Merge.
2009-03-04 blanchet 2009-03-04 Merge.
2009-02-21 nipkow 2009-02-21 Removed subsumed lemmas
2009-02-18 huffman 2009-02-18 generalize int_dvd_cancel_factor simproc to idom class
2009-02-17 huffman 2009-02-17 lemmas abs_dvd_iff, dvd_abs_iff
2009-02-16 haftmann 2009-02-16 more default simp rules for sgn
2009-02-15 nipkow 2009-02-15 dvd and setprod lemmas
2009-02-14 huffman 2009-02-14 generalize lemma fps_square_eq_iff, move to Ring_and_Field
2009-02-13 huffman 2009-02-13 add class cancel_comm_monoid_add
2009-02-08 nipkow 2009-02-08 added noatps
2009-01-31 nipkow 2009-01-31 added some simp rules
2009-01-28 nipkow 2009-01-28 merged - resolving conflics
2009-01-28 nipkow 2009-01-28 Replaced group_ and ring_simps by algebra_simps; removed compare_rls - use algebra_simps now
2009-01-28 haftmann 2009-01-28 added lemma abs_sng
2009-01-12 huffman 2009-01-12 change dvd_minus_iff, minus_dvd_iff from [iff] to [simp] (due to problems with Library/Primes.thy)
2009-01-12 huffman 2009-01-12 declare dvd_minus_iff and minus_dvd_iff [iff]
2009-01-08 huffman 2009-01-08 add lemma dvd_diff to class comm_ring_1
2009-01-08 huffman 2009-01-08 add lemmas dvd_minus_iff and minus_dvd_iff in class comm_ring_1
2009-01-08 huffman 2009-01-08 move lemmas mult_minus{left,right} inside class ring
2009-01-08 huffman 2009-01-08 clean up division_ring proofs
2008-11-17 haftmann 2008-11-17 tuned unfold_locales invocation
2008-10-10 haftmann 2008-10-10 tuned default rules of (dvd)
2008-09-05 huffman 2008-09-05 instances comm_semiring_0_cancel < comm_semiring_0, comm_ring < comm_semiring_0_cancel
2008-07-18 haftmann 2008-07-18 moved op dvd to theory Ring_and_Field; generalized a couple of lemmas
2008-07-10 huffman 2008-07-10 by intro_locales -> ..
2008-03-15 haftmann 2008-03-15 continued localization
2008-03-07 haftmann 2008-03-07 clarified proposition
2008-03-03 haftmann 2008-03-03 continued localization
2008-01-15 haftmann 2008-01-15 further localization
2008-01-02 haftmann 2008-01-02 splitted class uminus from class minus
2007-12-06 nipkow 2007-12-06 R&F: added sgn lemma Prefix: sledge-hammered
2007-11-30 haftmann 2007-11-30 using intro_locales instead of unfold_locales if appropriate
2007-11-21 haftmann 2007-11-21 dropped diagnostic commands
2007-11-06 haftmann 2007-11-06 removed subclass edge ordered_ring < lordered_ring
2007-11-02 haftmann 2007-11-02 proper reinitialisation after subclass
2007-10-30 haftmann 2007-10-30 fixed document preparation
2007-10-30 haftmann 2007-10-30 continued localization
2007-10-25 haftmann 2007-10-25 various localizations
2007-10-25 haftmann 2007-10-25 localized further
2007-10-23 haftmann 2007-10-23 partially localized
2007-10-18 haftmann 2007-10-18 moved lemmas to OrderedGroup.thy
2007-10-16 haftmann 2007-10-16 global class syntax
2007-09-29 haftmann 2007-09-29 proper syntax during class specification
2007-09-01 wenzelm 2007-09-01 linorder_neqE_ordered_idom: proper proof, avoid illegal schematic type vars;
2007-09-01 nipkow 2007-09-01 final(?) iteration of sgn saga.
2007-08-30 nipkow 2007-08-30 added constant sgn
2007-08-24 paulson 2007-08-24 revised blacklisting for ATP linkup
2007-08-24 haftmann 2007-08-24 moved class dense_linear_order to Orderings.thy
2007-08-15 paulson 2007-08-15 ATP blacklisting is now in theory data, attribute noatp
2007-07-20 haftmann 2007-07-20 split class abs from class minus
2007-07-03 huffman 2007-07-03 convert instance proofs to Isar style