src/HOL/Power.thy
2012-03-30 huffman 2012-03-30 add constant pred_numeral k = numeral k - (1::nat); replace several simp rules from Nat_Numeral.thy with new ones that use pred_numeral
2012-03-29 huffman 2012-03-29 move many lemmas from Nat_Numeral.thy to Power.thy or Num.thy
2012-03-29 huffman 2012-03-29 bootstrap Num.thy before Power.thy; move lemmas about powers into Power.thy
2011-10-21 bulwahn 2011-10-21 replacing code_inline by code_unfold, removing obsolete code_unfold, code_inline del now that the ancient code generator is removed
2011-01-14 wenzelm 2011-01-14 eliminated global prems; tuned proofs;
2010-09-16 wenzelm 2010-09-16 Isar "default" step needs to fail for solved problems, for clear distinction of '.' and '..' for example -- amending lapse introduced in 9de4d64eee3b (April 2004);
2010-04-26 haftmann 2010-04-26 use new classes (linordered_)field_inverse_zero
2010-04-26 haftmann 2010-04-26 class division_ring_inverse_zero
2010-03-18 blanchet 2010-03-18 now use "Named_Thms" for "noatp", and renamed "noatp" to "no_atp"
2010-02-18 huffman 2010-02-18 get rid of many duplicate simp rule warnings
2010-02-05 haftmann 2010-02-05 more consistent naming of type classes involving orderings (and lattices) -- c.f. NEWS
2009-10-30 haftmann 2009-10-30 tuned code setup
2009-10-28 haftmann 2009-10-28 moved lemmas for dvd on nat to theories Nat and Power
2009-07-14 haftmann 2009-07-14 code attributes use common underscore convention
2009-05-14 haftmann 2009-05-14 monomorphic code generation for power operations
2009-04-29 haftmann 2009-04-29 farewell to class recpower
2009-04-27 haftmann 2009-04-27 cleaned up theory power further
2009-04-26 haftmann 2009-04-26 fixed document generation
2009-04-26 haftmann 2009-04-26 cleaned up Power theory
2009-04-22 haftmann 2009-04-22 power operation defined generic
2009-03-26 paulson 2009-03-26 New theorems mostly concerning infinite series.
2009-03-13 huffman 2009-03-13 remove legacy ML bindings
2009-03-06 nipkow 2009-03-06 added lemmas
2009-03-04 huffman 2009-03-04 declare power_Suc [simp]; remove redundant type-specific versions of power_Suc
2009-03-04 blanchet 2009-03-04 Merge.
2009-03-04 blanchet 2009-03-04 Merge.
2009-02-23 huffman 2009-02-23 make proofs work whether or not One_nat_def is a simp rule; replace 1 with Suc 0 in the rhs of some simp rules
2009-02-22 nipkow 2009-02-22 added lemmas
2009-02-18 huffman 2009-02-18 generalize le_imp_power_dvd and power_le_dvd; move from Divides to Power
2009-01-21 haftmann 2009-01-21 no base sort in class import
2008-09-04 huffman 2008-09-04 add lemma power_Suc2; generalize power_minus from class comm_ring_1 to ring_1
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