src/HOL/Library/Formal_Power_Series.thy
Wed, 04 Jan 2017 21:28:29 +0100 haftmann reworked to provide auxiliary operations Euclidean_Algorithm.* to instantiate gcd etc. for euclidean rings
Wed, 04 Jan 2017 21:28:28 +0100 haftmann reshaped euclidean semiring into hierarchy of euclidean semirings culminating in uniquely determined euclidean divion
Sat, 17 Dec 2016 15:22:14 +0100 haftmann more fine-grained type class hierarchy for div and mod
Mon, 17 Oct 2016 17:33:07 +0200 nipkow setprod -> prod
Mon, 17 Oct 2016 11:46:22 +0200 nipkow setsum -> sum
Sun, 16 Oct 2016 09:31:05 +0200 haftmann more standardized theorem names for facts involving the div and mod identity
Sun, 16 Oct 2016 09:31:04 +0200 haftmann more standardized names
Mon, 19 Sep 2016 20:06:21 +0200 fleury left_distrib ~> distrib_right, right_distrib ~> distrib_left
Thu, 15 Sep 2016 11:48:20 +0200 nipkow renamed listsum -> sum_list, listprod ~> prod_list
Tue, 02 Aug 2016 21:30:30 +0200 wenzelm more symbols;
Fri, 22 Jul 2016 08:02:37 +0200 wenzelm tuned proofs -- avoid improper use of "this";
Sat, 09 Jul 2016 13:26:16 +0200 haftmann more lemmas to emphasize {0::nat..(<)n} as canonical representation of intervals on nat
Sat, 02 Jul 2016 20:22:25 +0200 haftmann simplified definitions of combinatorial functions
Thu, 16 Jun 2016 17:57:09 +0200 eberlm Various additions to polynomials, FPSs, Gamma function
Mon, 25 Apr 2016 16:09:26 +0200 wenzelm eliminated old 'def';
Tue, 01 Mar 2016 10:36:19 +0100 haftmann tuned bootstrap order to provide type classes in a more sensible order
Thu, 25 Feb 2016 16:44:53 +0100 eberlm Tuned Euclidean rings
Tue, 23 Feb 2016 16:25:08 +0100 nipkow more canonical names
Wed, 17 Feb 2016 21:51:56 +0100 haftmann prefer abbreviations for compound operators INFIMUM and SUPREMUM
Fri, 08 Jan 2016 17:41:04 +0100 hoelzl fix code generation for uniformity: uniformity is a non-computable pure data.
Fri, 08 Jan 2016 17:40:59 +0100 hoelzl add uniform spaces
Tue, 29 Dec 2015 23:04:53 +0100 wenzelm more symbols;
Sun, 27 Dec 2015 22:07:17 +0100 wenzelm discontinued ASCII replacement syntax <*>;
Mon, 07 Dec 2015 16:06:49 +0100 eberlm Generalised derivative rule for division on formal power series
Mon, 07 Dec 2015 10:38:04 +0100 wenzelm isabelle update_cartouches -c -t;
Fri, 13 Nov 2015 12:27:13 +0000 paulson Tweaks for "real": Removal of [iff] status for some lemmas, adding [simp] for others. Plus fixes.
Tue, 10 Nov 2015 14:43:29 +0000 paulson Merge
Tue, 10 Nov 2015 14:18:41 +0000 paulson Coercion "real" now has type nat => real only and is no longer overloaded. Type class "real_of" is gone. Many duplicate theorems removed.
Tue, 10 Nov 2015 14:46:11 +0100 eberlm subdegree/shift/cutoff and Euclidean ring instance for formal power series
Thu, 05 Nov 2015 10:39:49 +0100 wenzelm isabelle update_cartouches -c -t;
Mon, 02 Nov 2015 16:17:09 +0100 eberlm Added binomial identities to CONTRIBUTORS; small lemmas on of_int/pochhammer
Thu, 06 Aug 2015 23:56:48 +0200 haftmann slight cleanup of lemmas
Mon, 06 Jul 2015 22:57:34 +0200 wenzelm tuned proofs;
Wed, 24 Jun 2015 23:03:55 +0200 wenzelm tuned proofs -- less digits;
Mon, 22 Jun 2015 21:50:12 +0200 wenzelm tuned proofs;
Wed, 17 Jun 2015 18:58:46 +0200 wenzelm tuned proofs;
Wed, 17 Jun 2015 17:52:04 +0200 wenzelm tuned proofs;
Wed, 17 Jun 2015 11:03:05 +0200 wenzelm isabelle update_cartouches;
Thu, 30 Apr 2015 15:28:01 +0100 paulson tidying some messy proofs
Sat, 11 Apr 2015 11:56:40 +0100 paulson Overloading of ln and powr, but "approximation" no longer works for powr. Code generation also fails due to type ambiguity in scala.
Tue, 31 Mar 2015 21:54:32 +0200 haftmann given up separate type classes demanding `inverse 0 = 0`
Tue, 31 Mar 2015 15:00:03 +0100 paulson New material and binomial fix
Mon, 23 Mar 2015 19:05:14 +0100 haftmann explicit commutative additive inverse operation;
Wed, 18 Mar 2015 14:13:27 +0000 paulson Lots of new material on complex-valued functions. Modified simplification of (x/n)^k
Mon, 16 Mar 2015 15:30:00 +0000 paulson The factorial function, "fact", now has type "nat => 'a"
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
Sun, 02 Nov 2014 17:20:45 +0100 wenzelm modernized header;
Sun, 19 Oct 2014 18:05:26 +0200 haftmann prefer generic elimination rules for even/odd over specialized unfold rules for nat
Tue, 14 Oct 2014 08:23:23 +0200 haftmann legacy cleanup
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, 28 Jun 2014 09:16:42 +0200 haftmann fact consolidation
Fri, 30 May 2014 14:55:10 +0200 hoelzl introduce more powerful reindexing rules for big operators
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
Fri, 04 Apr 2014 17:58:25 +0100 paulson divide_minus_left divide_minus_right are in field_simps but are not default simprules
Wed, 29 Jan 2014 12:51:37 +0000 paulson Replacing the theory Library/Binomial by Number_Theory/Binomial
Fri, 06 Dec 2013 17:33:45 +0100 wenzelm tuned proofs;
Tue, 19 Nov 2013 10:05:53 +0100 haftmann eliminiated neg_numeral in favour of - (numeral _)
Sat, 16 Nov 2013 18:31:30 +0100 wenzelm tuned proofs;
less more (0) -100 -60 tip