src/HOL/Power.thy
2008-01-09 nipkow 2008-01-09 added simp attributes
2008-01-05 haftmann 2008-01-05 more instantiation
2007-10-30 haftmann 2007-10-30 simplified proof
2007-10-23 nipkow 2007-10-23 went back to >0
2007-10-21 nipkow 2007-10-21 Eliminated most of the neq0_conv occurrences. As a result, many theorems had to be rephrased with ~= 0 instead of > 0.
2007-10-16 haftmann 2007-10-16 global class syntax
2007-10-12 haftmann 2007-10-12 moved class power to theory Power
2007-08-21 huffman 2007-08-21 add lemma one_less_power
2007-08-15 paulson 2007-08-15 ATP blacklisting is now in theory data, attribute noatp
2007-07-03 huffman 2007-07-03 rename class dom to ring_1_no_zero_divisors
2007-06-20 huffman 2007-06-20 change simp rules for of_nat to work like int did previously (reorient of_nat_Suc, remove of_nat_mult [simp]); preserve original variable names in legacy int theorems
2007-06-11 huffman 2007-06-11 add lemma of_nat_power
2007-06-01 haftmann 2007-06-01 tuned
2007-05-17 huffman 2007-05-17 generalize class restrictions on some lemmas
2007-05-17 huffman 2007-05-17 generalize some lemmas from field to division_ring
2007-05-14 huffman 2007-05-14 tuned
2007-05-13 huffman 2007-05-13 add lemma power_eq_imp_eq_base
2007-05-08 huffman 2007-05-08 add lemma power_less_imp_less_base
2007-04-10 huffman 2007-04-10 removed unnecessary premise from power_le_imp_le_base
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)