src/HOL/Rings.thy
Sat, 28 Mar 2015 20:43:19 +0100 haftmann dropped long-outdated comments
Mon, 23 Mar 2015 19:05:14 +0100 haftmann distributivity of partial minus establishes desired properties of dvd in semirings
Thu, 19 Feb 2015 11:53:36 +0100 haftmann establish unique preferred fact names
Wed, 18 Feb 2015 22:46:48 +0100 haftmann eliminated fact duplicates
Sat, 14 Feb 2015 10:24:15 +0100 haftmann fact consolidation
Mon, 17 Nov 2014 14:55:33 +0100 haftmann generalized lemmas (particularly concerning dvd) as far as appropriate
Thu, 13 Nov 2014 17:19:52 +0100 hoelzl import general theorems from AFP/Markov_Models
Sat, 08 Nov 2014 16:53:26 +0100 haftmann equivalence rules for structures without zero divisors
Sun, 02 Nov 2014 18:21:45 +0100 wenzelm modernized header uniformly as section;
Fri, 24 Oct 2014 15:07:51 +0200 hoelzl use NO_MATCH-simproc for distribution rules in field_simps, otherwise field_simps on '(a / (c + d)) * (e + f)' can be non-terminating
Sun, 12 Oct 2014 17:05:34 +0200 haftmann generalized and consolidated some theorems concerning divisibility
Sun, 12 Oct 2014 16:31:28 +0200 haftmann more facts about abstract divisibility
Sun, 07 Sep 2014 09:49:01 +0200 haftmann generalized
Sat, 06 Sep 2014 20:12:32 +0200 haftmann added various facts
Sat, 05 Jul 2014 11:01:53 +0200 haftmann prefer ac_simps collections over separate name bindings for add and mult
Fri, 04 Jul 2014 20:18:47 +0200 haftmann reduced name variants for assoc and commute on plus and mult
Sat, 12 Apr 2014 17:26:27 +0200 nipkow made mult_pos_pos a simp rule
Fri, 11 Apr 2014 13:36:57 +0200 nipkow made mult_nonneg_nonneg a simp rule
Wed, 09 Apr 2014 09:37:48 +0200 hoelzl field_simps: better support for negation and division, and power
Wed, 19 Mar 2014 17:06:02 +0000 paulson Some rationalisation of basic lemmas
Tue, 04 Mar 2014 16:16:05 -0800 huffman fix typo
Thu, 30 Jan 2014 16:09:03 +0100 haftmann split rules for of_bool, similar to if
Mon, 09 Dec 2013 12:22:23 +0100 wenzelm more antiquotations;
Tue, 19 Nov 2013 10:05:53 +0100 haftmann eliminiated neg_numeral in favour of - (numeral _)
Mon, 04 Nov 2013 20:10:09 +0100 haftmann fact generalization and name consolidation
Fri, 01 Nov 2013 18:51:14 +0100 haftmann more simplification rules on unary and binary minus
Thu, 31 Oct 2013 11:44:20 +0100 haftmann generalized of_bool conversion
Fri, 18 Oct 2013 10:43:20 +0200 blanchet killed most "no_atp", to make Sledgehammer more complete
Sun, 23 Jun 2013 21:16:07 +0200 haftmann migration from code_(const|type|class|instance) to code_printing and from code_module to code_identifier
Tue, 26 Mar 2013 12:20:54 +0100 hoelzl move real_isLub_unique to isLub_unique in Lubs; real_sum_of_halves to RealDef; abs_diff_less_iff to Rings
Fri, 07 Dec 2012 15:53:28 +0100 nipkow corrected nonsensical associativity of `` and dvd
Fri, 19 Oct 2012 15:12:52 +0200 webertj Renamed {left,right}_distrib to distrib_{right,left}.
Tue, 13 Sep 2011 17:07:33 -0700 huffman tuned proofs
Sat, 20 Aug 2011 15:19:35 -0700 huffman replace lemma realpow_two_diff with new lemma square_diff_square_factored
Sat, 20 Aug 2011 10:08:47 -0700 huffman rename real_squared_diff_one_factored to square_diff_one_factored and move to Rings.thy
Mon, 08 Aug 2011 09:52:09 -0700 huffman moved division ring stuff from Rings.thy to Fields.thy
Mon, 23 Aug 2010 11:17:13 +0200 haftmann dropped type classes mult_mono and mult_mono1; tuned names of technical rule duplicates
Mon, 12 Jul 2010 10:48:37 +0200 haftmann dropped superfluous [code del]s
Mon, 17 May 2010 18:59:59 -0700 huffman declare add_nonneg_nonneg [simp]; remove now-redundant lemmas realpow_two_le_order(2)
Mon, 17 May 2010 08:45:46 -0700 huffman remove simp attribute from square_eq_1_iff
Mon, 10 May 2010 21:27:52 -0700 huffman move lemma real_mult_is_one to Rings.thy, renamed to square_eq_1_iff
Thu, 06 May 2010 23:11:56 +0200 haftmann moved some lemmas from Groebner_Basis here
Tue, 20 Apr 2010 17:58:34 +0200 hoelzl Generalize swap_inj_on; add simps for Times; add Ex_list_of_length, log_inj; Added missing locale edges for linordered semiring with 1.
Mon, 26 Apr 2010 11:34:15 +0200 haftmann dropped group_simps, ring_simps, field_eq_simps; classes division_ring_inverse_zero, field_inverse_zero, linordered_field_inverse_zero
Fri, 23 Apr 2010 15:17:59 +0200 haftmann less special treatment of times_divide_eq [simp]
Fri, 23 Apr 2010 13:58:14 +0200 haftmann more localization; factored out lemmas for division_ring
Thu, 18 Mar 2010 12:58:52 +0100 blanchet now use "Named_Thms" for "noatp", and renamed "noatp" to "no_atp"
Sat, 06 Mar 2010 18:24:30 -0800 huffman generalize some lemmas from class linordered_ring_strict to linordered_ring
Mon, 22 Feb 2010 15:53:18 +0100 haftmann tuned text
Thu, 18 Feb 2010 14:21:44 -0800 huffman get rid of many duplicate simp rule warnings
Wed, 10 Feb 2010 15:52:12 +0100 haftmann dropped last occurence of the linlinordered accident
Wed, 10 Feb 2010 14:12:04 +0100 haftmann moved less_eq, less to Orderings.thy; moved abs, sgn to Groups.thy
Wed, 10 Feb 2010 08:49:26 +0100 haftmann division ring assumes divide_inverse
Mon, 08 Feb 2010 17:12:38 +0100 haftmann renamed OrderedGroup to Groups; split theory Ring_and_Field into Rings Fields
less more (0) tip