src/HOL/Library/Formal_Power_Series.thy
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 _)
2013-11-16 wenzelm 2013-11-16 tuned proofs;
2013-11-05 hoelzl 2013-11-05 move Lubs from HOL to HOL-Library (replaced by conditionally complete lattices)
2013-11-01 haftmann 2013-11-01 more simplification rules on unary and binary minus
2013-09-03 wenzelm 2013-09-03 tuned proofs -- clarified flow of facts wrt. calculation;
2013-08-25 wenzelm 2013-08-25 tuned proofs;
2013-08-25 wenzelm 2013-08-25 tuned proofs;
2013-08-18 wenzelm 2013-08-18 more symbols;
2013-08-07 wenzelm 2013-08-07 tuned proofs;
2013-08-07 wenzelm 2013-08-07 tuned proofs;
2013-08-07 wenzelm 2013-08-07 tuned proofs;
2013-03-26 wenzelm 2013-03-26 tuned imports;
2013-03-23 haftmann 2013-03-23 fundamental revision of big operators on sets
2013-02-13 immler 2013-02-13 complete metric for formal power series
2012-10-19 webertj 2012-10-19 Renamed {left,right}_distrib to distrib_{right,left}.
2012-10-12 wenzelm 2012-10-12 discontinued obsolete typedef (open) syntax;
2012-08-10 wenzelm 2012-08-10 tuned proofs;
2012-03-30 huffman 2012-03-30 removed redundant nat-specific copies of theorems
2012-03-25 huffman 2012-03-25 merged fork with new numeral representation (see NEWS)
2012-03-02 bulwahn 2012-03-02 removing finiteness goals
2012-01-06 haftmann 2012-01-06 prefer listsum over foldl plus 0
2011-08-12 huffman 2011-08-12 make more HOL theories work with separate set type
2011-03-13 wenzelm 2011-03-13 tuned headers;
2010-09-13 nipkow 2010-09-13 renamed lemmas: ext_iff -> fun_eq_iff, set_ext_iff -> set_eq_iff, set_ext -> set_eqI
2010-09-07 nipkow 2010-09-07 expand_fun_eq -> ext_iff expand_set_eq -> set_ext_iff Naming in line now with multisets
2010-06-08 haftmann 2010-06-08 tuned quotes, antiquotations and whitespace
2010-05-11 haftmann 2010-05-11 renamed former Int.int_induct to Int.int_of_nat_induct, former Presburger.int_induct to Int.int_induct: is more conservative and more natural than the intermediate solution
2010-05-11 haftmann 2010-05-11 theorem Presburger.int_induct has been renamed to Int.int_bidirectional_induct
2010-04-26 haftmann 2010-04-26 use new classes (linordered_)field_inverse_zero
2010-04-26 haftmann 2010-04-26 dropped group_simps, ring_simps, field_eq_simps
2010-04-23 haftmann 2010-04-23 epheremal replacement of field_simps by field_eq_simps; dropped old division_by_zero instance
2010-04-23 haftmann 2010-04-23 epheremal replacement of field_simps by field_eq_simps
2010-02-17 huffman 2010-02-17 fix more looping simp rules
2009-10-17 wenzelm 2009-10-17 eliminated hard tabulators, guessing at each author's individual tab-width; tuned headers;
2009-08-31 nipkow 2009-08-31 tuned the simp rules for Int involving insert and intervals.
2009-08-26 chaieb 2009-08-26 merged
2009-05-19 chaieb 2009-05-19 merged
2009-05-19 chaieb 2009-05-19 Derivative of general reverses
2009-07-23 chaieb 2009-07-23 fixed proof --- fact_setprod removed for fact_altdef_nat