src/HOL/Library/Formal_Power_Series.thy
2017-04-04 eberlm 2017-04-04 moved AFP material to Formal_Power_Series; renamed E/L/F in Formal_Power_Series
2017-01-04 haftmann 2017-01-04 reworked to provide auxiliary operations Euclidean_Algorithm.* to instantiate gcd etc. for euclidean rings
2017-01-04 haftmann 2017-01-04 reshaped euclidean semiring into hierarchy of euclidean semirings culminating in uniquely determined euclidean divion
2016-12-17 haftmann 2016-12-17 more fine-grained type class hierarchy for div and mod
2016-10-17 nipkow 2016-10-17 setprod -> prod
2016-10-17 nipkow 2016-10-17 setsum -> sum
2016-10-16 haftmann 2016-10-16 more standardized theorem names for facts involving the div and mod identity
2016-10-16 haftmann 2016-10-16 more standardized names
2016-09-19 fleury 2016-09-19 left_distrib ~> distrib_right, right_distrib ~> distrib_left
2016-09-15 nipkow 2016-09-15 renamed listsum -> sum_list, listprod ~> prod_list
2016-08-02 wenzelm 2016-08-02 more symbols;
2016-07-22 wenzelm 2016-07-22 tuned proofs -- avoid improper use of "this";
2016-07-09 haftmann 2016-07-09 more lemmas to emphasize {0::nat..(<)n} as canonical representation of intervals on nat * * * more rules for setsum, setprod on intervals
2016-07-02 haftmann 2016-07-02 simplified definitions of combinatorial functions
2016-06-16 eberlm 2016-06-16 Various additions to polynomials, FPSs, Gamma function
2016-04-25 wenzelm 2016-04-25 eliminated old 'def'; tuned comments;
2016-03-01 haftmann 2016-03-01 tuned bootstrap order to provide type classes in a more sensible order
2016-02-25 eberlm 2016-02-25 Tuned Euclidean rings
2016-02-23 nipkow 2016-02-23 more canonical names
2016-02-17 haftmann 2016-02-17 prefer abbreviations for compound operators INFIMUM and SUPREMUM
2016-01-08 hoelzl 2016-01-08 fix code generation for uniformity: uniformity is a non-computable pure data.
2016-01-08 hoelzl 2016-01-08 add uniform spaces
2015-12-29 wenzelm 2015-12-29 more symbols;
2015-12-27 wenzelm 2015-12-27 discontinued ASCII replacement syntax <*>;
2015-12-07 eberlm 2015-12-07 Generalised derivative rule for division on formal power series
2015-12-07 wenzelm 2015-12-07 isabelle update_cartouches -c -t;
2015-11-13 paulson 2015-11-13 Tweaks for "real": Removal of [iff] status for some lemmas, adding [simp] for others. Plus fixes.
2015-11-10 paulson 2015-11-10 Merge
2015-11-10 paulson 2015-11-10 Coercion "real" now has type nat => real only and is no longer overloaded. Type class "real_of" is gone. Many duplicate theorems removed.
2015-11-10 eberlm 2015-11-10 subdegree/shift/cutoff and Euclidean ring instance for formal power series
2015-11-05 wenzelm 2015-11-05 isabelle update_cartouches -c -t;
2015-11-02 eberlm 2015-11-02 Added binomial identities to CONTRIBUTORS; small lemmas on of_int/pochhammer
2015-08-06 haftmann 2015-08-06 slight cleanup of lemmas
2015-07-06 wenzelm 2015-07-06 tuned proofs;
2015-06-24 wenzelm 2015-06-24 tuned proofs -- less digits;
2015-06-22 wenzelm 2015-06-22 tuned proofs;
2015-06-17 wenzelm 2015-06-17 tuned proofs;
2015-06-17 wenzelm 2015-06-17 tuned proofs;
2015-06-17 wenzelm 2015-06-17 isabelle update_cartouches;
2015-04-30 paulson 2015-04-30 tidying some messy proofs
2015-04-11 paulson 2015-04-11 Overloading of ln and powr, but "approximation" no longer works for powr. Code generation also fails due to type ambiguity in scala.
2015-03-31 haftmann 2015-03-31 given up separate type classes demanding `inverse 0 = 0`
2015-03-31 paulson 2015-03-31 New material and binomial fix
2015-03-23 haftmann 2015-03-23 explicit commutative additive inverse operation; more explicit focal point for commutative monoids with an inverse operation
2015-03-18 paulson 2015-03-18 Lots of new material on complex-valued functions. Modified simplification of (x/n)^k
2015-03-16 paulson 2015-03-16 The factorial function, "fact", now has type "nat => 'a"
2015-03-10 paulson 2015-03-10 Removal of the file HOL/Number_Theory/Binomial!! And class field_char_0 now declared in Int.thy
2014-11-02 wenzelm 2014-11-02 modernized header;
2014-10-19 haftmann 2014-10-19 prefer generic elimination rules for even/odd over specialized unfold rules for nat
2014-10-14 haftmann 2014-10-14 legacy cleanup
2014-07-05 haftmann 2014-07-05 prefer ac_simps collections over separate name bindings for add and mult
2014-07-04 haftmann 2014-07-04 reduced name variants for assoc and commute on plus and mult
2014-06-28 haftmann 2014-06-28 fact consolidation
2014-05-30 hoelzl 2014-05-30 introduce more powerful reindexing rules for big operators
2014-04-09 hoelzl 2014-04-09 field_simps: better support for negation and division, and power
2014-04-09 hoelzl 2014-04-09 revert c1bbd3e22226, a14831ac3023, and 36489d77c484: divide_minus_left/right are again simp rules
2014-04-04 paulson 2014-04-04 divide_minus_left divide_minus_right are in field_simps but are not default simprules
2014-01-29 paulson 2014-01-29 Replacing the theory Library/Binomial by Number_Theory/Binomial
2013-12-06 wenzelm 2013-12-06 tuned proofs;
2013-11-19 haftmann 2013-11-19 eliminiated neg_numeral in favour of - (numeral _)