src/HOL/Ring_and_Field.thy
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
2007-07-03 huffman 2007-07-03 rename class dom to ring_1_no_zero_divisors
2007-07-03 huffman 2007-07-03 instance pordered_comm_ring < pordered_ring
2007-06-30 obua 2007-06-30 added ordered_ring and ordered_semiring
2007-06-25 nipkow 2007-06-25 removed redundant lemmas
2007-06-24 nipkow 2007-06-24 tex problem fixed
2007-06-24 nipkow 2007-06-24 tuned and used field_simps
2007-06-23 nipkow 2007-06-23 tuned and renamed group_eq_simps and ring_eq_simps
2007-06-17 nipkow 2007-06-17 tuned laws for cancellation in divisions for fields.
2007-06-17 chaieb 2007-06-17 added theorems nonzero_mult_divide_cancel_right' nonzero_mult_divide_cancel_left' ordered_field_no_lb ordered_field_no_ub