src/HOL/Ring_and_Field.thy
Sat, 21 Feb 2009 20:52:30 +0100 nipkow Removed subsumed lemmas
Wed, 18 Feb 2009 15:01:53 -0800 huffman generalize int_dvd_cancel_factor simproc to idom class
Tue, 17 Feb 2009 06:59:33 -0800 huffman lemmas abs_dvd_iff, dvd_abs_iff
Mon, 16 Feb 2009 19:11:55 +0100 haftmann more default simp rules for sgn
Sun, 15 Feb 2009 22:58:02 +0100 nipkow dvd and setprod lemmas
Sat, 14 Feb 2009 19:01:31 -0800 huffman generalize lemma fps_square_eq_iff, move to Ring_and_Field
Fri, 13 Feb 2009 14:12:00 -0800 huffman add class cancel_comm_monoid_add
Sun, 08 Feb 2009 11:59:26 +0100 nipkow added noatps
Sat, 31 Jan 2009 09:04:16 +0100 nipkow added some simp rules
Wed, 28 Jan 2009 16:57:12 +0100 nipkow merged - resolving conflics
Wed, 28 Jan 2009 16:29:16 +0100 nipkow Replaced group_ and ring_simps by algebra_simps;
Wed, 28 Jan 2009 11:02:12 +0100 haftmann added lemma abs_sng
Mon, 12 Jan 2009 23:36:30 -0800 huffman change dvd_minus_iff, minus_dvd_iff from [iff] to [simp] (due to problems with Library/Primes.thy)
Mon, 12 Jan 2009 12:10:41 -0800 huffman declare dvd_minus_iff and minus_dvd_iff [iff]
Thu, 08 Jan 2009 10:43:09 -0800 huffman add lemma dvd_diff to class comm_ring_1
Thu, 08 Jan 2009 10:26:50 -0800 huffman add lemmas dvd_minus_iff and minus_dvd_iff in class comm_ring_1
Thu, 08 Jan 2009 10:07:39 -0800 huffman move lemmas mult_minus{left,right} inside class ring
Thu, 08 Jan 2009 09:58:36 -0800 huffman clean up division_ring proofs
Mon, 17 Nov 2008 17:00:55 +0100 haftmann tuned unfold_locales invocation
Fri, 10 Oct 2008 06:45:48 +0200 haftmann tuned default rules of (dvd)
Fri, 05 Sep 2008 00:19:50 +0200 huffman instances comm_semiring_0_cancel < comm_semiring_0, comm_ring < comm_semiring_0_cancel
Fri, 18 Jul 2008 18:25:53 +0200 haftmann moved op dvd to theory Ring_and_Field; generalized a couple of lemmas
Thu, 10 Jul 2008 07:15:19 +0200 huffman by intro_locales -> ..
Sat, 15 Mar 2008 08:11:15 +0100 haftmann continued localization
Fri, 07 Mar 2008 13:53:03 +0100 haftmann clarified proposition
Mon, 03 Mar 2008 15:37:14 +0100 haftmann continued localization
Tue, 15 Jan 2008 16:19:20 +0100 haftmann further localization
Wed, 02 Jan 2008 15:14:02 +0100 haftmann splitted class uminus from class minus
Thu, 06 Dec 2007 19:58:21 +0100 nipkow R&F: added sgn lemma
Fri, 30 Nov 2007 20:13:06 +0100 haftmann using intro_locales instead of unfold_locales if appropriate
Wed, 21 Nov 2007 13:42:31 +0100 haftmann dropped diagnostic commands
Tue, 06 Nov 2007 08:47:30 +0100 haftmann removed subclass edge ordered_ring < lordered_ring
Fri, 02 Nov 2007 18:52:58 +0100 haftmann proper reinitialisation after subclass
Tue, 30 Oct 2007 12:14:24 +0100 haftmann fixed document preparation
Tue, 30 Oct 2007 08:45:54 +0100 haftmann continued localization
Thu, 25 Oct 2007 19:27:50 +0200 haftmann various localizations
Thu, 25 Oct 2007 13:52:00 +0200 haftmann localized further
Tue, 23 Oct 2007 11:48:08 +0200 haftmann partially localized
Thu, 18 Oct 2007 09:20:58 +0200 haftmann moved lemmas to OrderedGroup.thy
Tue, 16 Oct 2007 23:12:45 +0200 haftmann global class syntax
Sat, 29 Sep 2007 08:58:51 +0200 haftmann proper syntax during class specification
Sat, 01 Sep 2007 18:17:38 +0200 wenzelm linorder_neqE_ordered_idom: proper proof, avoid illegal schematic type vars;
Sat, 01 Sep 2007 01:21:48 +0200 nipkow final(?) iteration of sgn saga.
Thu, 30 Aug 2007 21:43:31 +0200 nipkow added constant sgn
Fri, 24 Aug 2007 14:21:33 +0200 paulson revised blacklisting for ATP linkup
Fri, 24 Aug 2007 14:14:18 +0200 haftmann moved class dense_linear_order to Orderings.thy
Wed, 15 Aug 2007 12:52:56 +0200 paulson ATP blacklisting is now in theory data, attribute noatp
Fri, 20 Jul 2007 14:28:01 +0200 haftmann split class abs from class minus
Tue, 03 Jul 2007 18:42:09 +0200 huffman convert instance proofs to Isar style
Tue, 03 Jul 2007 17:28:36 +0200 huffman rename class dom to ring_1_no_zero_divisors
Tue, 03 Jul 2007 01:26:06 +0200 huffman instance pordered_comm_ring < pordered_ring
Sat, 30 Jun 2007 17:30:10 +0200 obua added ordered_ring and ordered_semiring
Mon, 25 Jun 2007 15:19:18 +0200 nipkow removed redundant lemmas
Sun, 24 Jun 2007 21:15:55 +0200 nipkow tex problem fixed
Sun, 24 Jun 2007 20:55:41 +0200 nipkow tuned and used field_simps
Sat, 23 Jun 2007 19:33:22 +0200 nipkow tuned and renamed group_eq_simps and ring_eq_simps
Sun, 17 Jun 2007 18:47:03 +0200 nipkow tuned laws for cancellation in divisions for fields.
Sun, 17 Jun 2007 13:39:29 +0200 chaieb added theorems nonzero_mult_divide_cancel_right' nonzero_mult_divide_cancel_left' ordered_field_no_lb ordered_field_no_ub
Sat, 16 Jun 2007 15:01:54 +0200 nipkow The simprocs "divide_cancel_factor" and "ring_eq_cancel_factor" no
Fri, 15 Jun 2007 15:10:32 +0200 nipkow made divide_self a simp rule
less more (0) -100 -60 tip