src/HOL/Power.thy
19 months ago haftmann 2017-10-30 tuned some proofs and added some lemmas
20 months ago immler 2017-10-24 generalized lemmas cancelling real_of_int/real in (in)equalities with power; completed set of related simp rules; lemmas about floorlog/bitlen
2017-02-27 paulson 2017-02-27 Some new lemmas thanks to Lukas Bulwahn. Also, NEWS.
2017-01-29 wenzelm 2017-01-29 tuned proof;
2016-12-31 haftmann 2016-12-31 more elementary rules about div / mod on int
2016-10-06 nipkow 2016-10-06 moved lemmas
2016-09-18 haftmann 2016-09-18 more generic algebraic lemmas
2016-08-10 wenzelm 2016-08-10 misc tuning and modernization;
2016-08-10 nipkow 2016-08-10 "split add" -> "split"
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-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-18 haftmann 2016-02-18 more theorems
2016-02-17 haftmann 2016-02-17 generalized some lemmas; moved some lemmas in more appropriate places; deleted potentially dangerous simp rule
2016-01-06 hoelzl 2016-01-06 add the proof of the central limit theorem
2015-12-28 wenzelm 2015-12-28 former "xsymbols" syntax is used by default, and ASCII replacement syntax with print mode "ASCII";
2015-12-28 wenzelm 2015-12-28 prefer symbols for "abs";
2015-12-07 wenzelm 2015-12-07 isabelle update_cartouches -c -t;
2015-11-17 paulson 2015-11-17 Removed some legacy theorems; minor adjustments to simplification rules; new material on homotopic paths
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-02 eberlm 2015-11-02 Rounding function, uniform limits, cotangent, binomial identities
2015-10-09 wenzelm 2015-10-09 discontinued specific HTML syntax;
2015-09-01 wenzelm 2015-09-01 eliminated \<Colon>;
2015-08-19 paulson 2015-08-19 New material and fixes related to the forthcoming Stone-Weierstrass development
2015-08-06 haftmann 2015-08-06 slight cleanup of lemmas
2015-08-06 haftmann 2015-08-06 obsolete since no code generator without dictionary construction left
2015-07-18 wenzelm 2015-07-18 isabelle update_cartouches;
2015-07-08 haftmann 2015-07-08 moved normalization and unit_factor into Main HOL corpus
2015-04-29 paulson 2015-04-29 Tidying. Improved simplification for numerals, esp in exponents.
2015-03-31 haftmann 2015-03-31 given up separate type classes demanding `inverse 0 = 0`
2015-03-31 paulson 2015-03-31 rationalised and generalised some theorems concerning abs and x^2.
2015-03-18 paulson 2015-03-18 Lots of new material on complex-valued functions. Modified simplification of (x/n)^k
2014-11-17 haftmann 2014-11-17 generalized lemmas (particularly concerning dvd) as far as appropriate
2014-11-02 wenzelm 2014-11-02 modernized header uniformly as section;
2014-10-26 haftmann 2014-10-26 eliminated redundancies; more simp rules
2014-10-13 immler 2014-10-13 relaxed class constraints for exp
2014-09-24 haftmann 2014-09-24 added lemmas
2014-09-21 haftmann 2014-09-21 explicit separation of signed and unsigned numerals using existing lexical categories num and xnum
2014-09-03 blanchet 2014-09-03 moved old datatype material around
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-04-12 nipkow 2014-04-12 made mult_pos_pos a simp rule
2014-04-11 nipkow 2014-04-11 made mult_nonneg_nonneg a simp rule
2014-04-09 hoelzl 2014-04-09 add divide_simps
2014-04-09 hoelzl 2014-04-09 field_simps: better support for negation and division, and power
2014-02-28 traytel 2014-02-28 load Metis a little later
2014-02-24 paulson 2014-02-24 A few lemmas about summations, etc.
2014-01-21 traytel 2014-01-21 removed theory dependency of BNF_LFP on Datatype
2013-11-19 haftmann 2013-11-19 eliminiated neg_numeral in favour of - (numeral _)
2013-11-04 haftmann 2013-11-04 streamlined setup of linear arithmetic
2013-10-18 blanchet 2013-10-18 killed most "no_atp", to make Sledgehammer more complete
2013-08-18 wenzelm 2013-08-18 more symbols;
2013-08-13 wenzelm 2013-08-13 standardized symbols via "isabelle update_sub_sup", excluding src/Pure and src/Tools/WWW_Find;
2013-06-23 haftmann 2013-06-23 migration from code_(const|type|class|instance) to code_printing and from code_module to code_identifier
2013-02-24 haftmann 2013-02-24 turned example into library for comparing growth of functions
2012-10-11 haftmann 2012-10-11 msetprod based directly on Multiset.fold; pretty syntax for msetprod_image
2012-04-01 huffman 2012-04-01 removed Nat_Numeral.thy, moving all theorems elsewhere
2012-03-31 huffman 2012-03-31 add lemma power_le_one
2012-03-30 huffman 2012-03-30 replace lemmas eval_nat_numeral with a simpler reformulation