src/HOL/Fields.thy
Fri, 14 Jun 2019 08:34:27 +0000 haftmann moved comment to approproiate place
Fri, 14 Jun 2019 08:34:27 +0000 haftmann removed outcommented example which seems not to work as advertized
Sat, 13 Apr 2019 08:43:33 +0000 haftmann backed out a93e6472ac9c, which does not bring anything substantial: division_ring is not commutative in multiplication but semidom_divide is
Tue, 09 Apr 2019 16:59:00 +0000 haftmann common type class for distributive division
Mon, 04 Feb 2019 17:19:04 +0100 Manuel Eberl Formal Laurent series and overhaul of Formal power series (due to Jeremy Sylvestre)
Sun, 06 Jan 2019 15:04:34 +0100 wenzelm isabelle update -u path_cartouches;
Fri, 04 Jan 2019 23:22:53 +0100 wenzelm isabelle update -u control_cartouches;
Sun, 23 Dec 2018 20:51:23 +0000 haftmann more rules
Fri, 29 Jun 2018 22:14:33 +0200 wenzelm merged;
Thu, 28 Jun 2018 21:05:56 +0200 wenzelm avoid pending shyps in global theory facts;
Thu, 28 Jun 2018 14:13:57 +0100 paulson Generalising and renaming some basic results
Mon, 09 Apr 2018 15:20:11 +0100 paulson Syntax for the special cases Min(A`I) and Max (A`I)
Sun, 26 Nov 2017 21:08:32 +0100 wenzelm more symbols;
Mon, 27 Feb 2017 17:17:26 +0000 paulson Some new lemmas thanks to Lukas Bulwahn. Also, NEWS.
Sat, 17 Dec 2016 15:22:13 +0100 haftmann restructured matter on polynomials and normalized fractions
Thu, 20 Oct 2016 20:03:32 +0200 haftmann more on sgn in linear ordered fields
Tue, 18 Oct 2016 18:48:53 +0200 haftmann suitable logical type class for abs, sgn
Wed, 28 Sep 2016 17:01:01 +0100 paulson new material connected with HOL Light measure theory, plus more rationalisation
Tue, 01 Mar 2016 10:36:19 +0100 haftmann tuned bootstrap order to provide type classes in a more sensible order
Wed, 17 Feb 2016 21:51:57 +0100 haftmann generalized some lemmas;
Mon, 28 Dec 2015 01:26:34 +0100 wenzelm prefer symbols for "abs";
Sun, 27 Dec 2015 17:16:21 +0100 wenzelm discontinued ASCII replacement syntax <->;
Mon, 07 Dec 2015 10:38:04 +0100 wenzelm isabelle update_cartouches -c -t;
Wed, 23 Sep 2015 14:11:35 +0100 paulson Useful facts about min/max, etc.
Tue, 01 Sep 2015 22:32:58 +0200 wenzelm eliminated \<Colon>;
Sat, 18 Jul 2015 22:58:50 +0200 wenzelm isabelle update_cartouches;
Wed, 08 Jul 2015 20:19:12 +0200 haftmann tuned facts
Thu, 25 Jun 2015 15:01:42 +0200 haftmann more theorems
Mon, 01 Jun 2015 18:59:22 +0200 haftmann implicit partial divison operation in integral domains
Mon, 01 Jun 2015 18:59:21 +0200 haftmann separate class for division operator, with particular syntax added in more specific classes
Tue, 31 Mar 2015 21:54:32 +0200 haftmann given up separate type classes demanding `inverse 0 = 0`
Mon, 23 Mar 2015 15:08:02 +0100 hoelzl fix parameter order of NO_MATCH
Tue, 10 Mar 2015 15:20:40 +0000 paulson Removal of the file HOL/Number_Theory/Binomial!! And class field_char_0 now declared in Int.thy
Thu, 19 Feb 2015 11:53:36 +0100 haftmann establish unique preferred fact names
Sun, 15 Feb 2015 17:01:22 +0100 haftmann times_divide_eq rules are already [simp] despite of comment
Sat, 14 Feb 2015 10:24:15 +0100 haftmann less warnings
Sun, 02 Nov 2014 18:21:45 +0100 wenzelm modernized header uniformly as section;
Wed, 29 Oct 2014 19:01:49 +0100 wenzelm modernized setup;
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
Thu, 02 Oct 2014 11:33:06 +0200 haftmann moved lemmas out of Int.thy which have nothing to do with int
Sat, 16 Aug 2014 14:12:39 +0200 wenzelm updated to named_theorems;
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
Mon, 14 Apr 2014 13:08:17 +0200 hoelzl added divide_nonneg_nonneg and co; made it a simp rule
Fri, 11 Apr 2014 22:53:33 +0200 nipkow made divide_pos_pos a simp rule
Wed, 09 Apr 2014 09:37:49 +0200 hoelzl add divide_simps
Wed, 09 Apr 2014 09:37:48 +0200 hoelzl field_simps: better support for negation and division, and power
Wed, 09 Apr 2014 09:37:47 +0200 hoelzl revert c1bbd3e22226, a14831ac3023, and 36489d77c484: divide_minus_left/right are again simp rules
Sun, 06 Apr 2014 21:01:33 +0200 nipkow tuned lemmas: more general class
Sun, 06 Apr 2014 17:18:57 +0200 nipkow made field_simps "more complete"
Sat, 05 Apr 2014 01:04:46 +0100 paulson A single [simp] to handle the case -a/-b.
Fri, 04 Apr 2014 17:58:25 +0100 paulson divide_minus_left divide_minus_right are in field_simps but are not default simprules
Thu, 03 Apr 2014 23:51:52 +0100 paulson removing simprule status for divide_minus_left and divide_minus_right
Wed, 02 Apr 2014 16:34:37 +0100 paulson New theorems for extracting quotients
Mon, 24 Feb 2014 15:45:55 +0000 paulson A few lemmas about summations, etc.
Fri, 01 Nov 2013 18:51:14 +0100 haftmann more simplification rules on unary and binary minus
Fri, 18 Oct 2013 10:43:20 +0200 blanchet killed most "no_atp", to make Sledgehammer more complete
Tue, 03 Sep 2013 01:12:40 +0200 wenzelm tuned proofs -- clarified flow of facts wrt. calculation;
Tue, 27 Aug 2013 14:37:56 +0200 hoelzl renamed typeclass dense_linorder to unbounded_dense_linorder
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
less more (0) -60 tip