src/HOL/Power.thy
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)