| Thu, 15 Nov 2001 16:12:49 +0100 |
paulson |
new theories from Jacques Fleuriot
|
file |
diff |
annotate
|
| Fri, 05 Oct 2001 21:52:39 +0200 |
wenzelm |
sane numerals (stage 1): added generic 1, removed 1' and 2 on nat,
|
file |
diff |
annotate
|
| Mon, 06 Aug 2001 13:43:24 +0200 |
nipkow |
turned translation for 1::nat into def.
|
file |
diff |
annotate
|
| Sat, 09 Jun 2001 08:42:29 +0200 |
paulson |
new material from the Sylow proof
|
file |
diff |
annotate
|
| Wed, 30 May 2001 10:48:59 +0200 |
bauerg |
injectivity of ^;
|
file |
diff |
annotate
|
| Sat, 19 May 2001 12:21:34 +0200 |
paulson |
power_le_dvd replaces power_less_dvd
|
file |
diff |
annotate
|
| 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
|