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