src/HOL/Power.ML
2000-08-17 paulson 2000-08-17 better rules for cancellation of common factors across comparisons
2000-07-24 wenzelm 2000-07-24 simpset_of NatDef.thy (why anyway?);
2000-05-23 paulson 2000-05-23 added type constraint ::nat because 0 is now overloaded
2000-05-12 paulson 2000-05-12 new theorem one_le_power
2000-03-13 wenzelm 2000-03-13 case_tac now subsumes both boolean and datatype cases;
2000-03-13 nipkow 2000-03-13 exhaust_tac -> cases_tac
1999-10-13 paulson 1999-10-13 deleted the redundant less_imp_binomial_eq_0
1999-07-26 paulson 1999-07-26 new facts about binomials
1999-07-01 paulson 1999-07-01 now div and mod are overloaded; dvd is polymorphic
1998-07-15 paulson 1998-07-15 Removal of leading "\!\!..." from most Goal commands
1998-06-22 wenzelm 1998-06-22 isatool fixgoal;
1997-11-03 wenzelm 1997-11-03 isatool fixclasimp;
1997-06-23 paulson 1997-06-23 Ran expandshort
1997-06-04 wenzelm 1997-06-04 eliminated non-ASCII;
1997-06-03 paulson 1997-06-03 New theory "Power" of exponentiation (and binomial coefficients)