src/HOL/Power.ML
Thu, 17 Aug 2000 12:02:01 +0200 paulson better rules for cancellation of common factors across comparisons
Mon, 24 Jul 2000 23:53:51 +0200 wenzelm simpset_of NatDef.thy (why anyway?);
Tue, 23 May 2000 18:06:22 +0200 paulson added type constraint ::nat because 0 is now overloaded
Fri, 12 May 2000 15:02:57 +0200 paulson new theorem one_le_power
Mon, 13 Mar 2000 16:23:34 +0100 wenzelm case_tac now subsumes both boolean and datatype cases;
Mon, 13 Mar 2000 12:51:10 +0100 nipkow exhaust_tac -> cases_tac
Wed, 13 Oct 1999 12:07:44 +0200 paulson deleted the redundant less_imp_binomial_eq_0
Mon, 26 Jul 1999 16:29:59 +0200 paulson new facts about binomials
Thu, 01 Jul 1999 10:33:50 +0200 paulson now div and mod are overloaded; dvd is polymorphic
Wed, 15 Jul 1998 10:15:13 +0200 paulson Removal of leading "\!\!..." from most Goal commands
Mon, 22 Jun 1998 17:26:46 +0200 wenzelm isatool fixgoal;
Mon, 03 Nov 1997 12:13:18 +0100 wenzelm isatool fixclasimp;
Mon, 23 Jun 1997 10:42:03 +0200 paulson Ran expandshort
Wed, 04 Jun 1997 16:03:54 +0200 wenzelm eliminated non-ASCII;
Tue, 03 Jun 1997 10:56:04 +0200 paulson New theory "Power" of exponentiation (and binomial coefficients)
less more (0) tip