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