src/HOL/Power.thy
2007-03-02 haftmann 2007-03-02 now using "class"
2006-11-22 haftmann 2006-11-22 cleanup
2006-11-18 haftmann 2006-11-18 moved dvd stuff to theory Divides
2006-11-07 krauss 2006-11-07 * Added annihilation axioms ("x * 0 = 0") to axclass semiring_0. Richer structures do not inherit from semiring_0 anymore, because anihilation is a theorem there, not an axiom. * Generalized axclass "recpower" to arbitrary monoid, not just commutative semirings.
2005-08-26 ballarin 2005-08-26 Lemmas on dvd, power and finite summation added or strengthened.
2005-07-13 paulson 2005-07-13 generlization of some "nat" theorems
2005-07-12 avigad 2005-07-12 added lemmas to OrderedGroup.thy (reasoning about signs, absolute value, triangle inequalities) added lemmas to Ring_and_Field.thy (reasoning about signs, fractions, etc.) renamed simplification rules for abs (abs_of_pos, etc.) renamed rules for multiplication and signs (mult_pos_pos, etc.) moved lemmas involving fractions from NatSimprocs.thy added setsum_mono3 to FiniteSet.thy added simplification rules for powers to Parity.thy
2005-07-07 nipkow 2005-07-07 linear arithmetic now takes "&" in assumptions apart.
2004-10-19 paulson 2004-10-19 converted some induct_tac to induct
2004-08-18 nipkow 2004-08-18 import -> imports
2004-08-16 nipkow 2004-08-16 New theory header syntax.
2004-07-20 paulson 2004-07-20 two new results
2004-06-24 paulson 2004-06-24 ringpower to recpower
2004-05-11 obua 2004-05-11 changes made due to new Ring_and_Field theory
2004-04-16 wenzelm 2004-04-16 tuned document;
2004-03-05 paulson 2004-03-05 tweaks
2004-01-12 paulson 2004-01-12 Added lemmas to Ring_and_Field with slightly modified simplification rules Deleted some little-used integer theorems, replacing them by the generic ones in Ring_and_Field Consolidated integer powers
2004-01-09 paulson 2004-01-09 Defining the type class "ringpower" and deleting superseded theorems for types nat, int, real, hypreal
2000-05-09 wenzelm 2000-05-09 named "op ^" definitions;
1999-10-13 paulson 1999-10-13 choose just as an infix
1998-07-24 berghofe 1998-07-24 Adapted to new datatype package.
1998-02-12 wenzelm 1998-02-12 *** empty log message ***
1997-06-03 paulson 1997-06-03 New theory "Power" of exponentiation (and binomial coefficients)