| Wed, 28 Nov 2001 00:37:40 +0100 |
wenzelm |
tuned declarations;
|
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
|
| Thu, 27 Sep 2001 18:43:17 +0200 |
wenzelm |
AddXIs [dvdI]; AddXEs [dvdE];
|
file |
diff |
annotate
|
| Mon, 06 Aug 2001 13:43:24 +0200 |
nipkow |
turned translation for 1::nat into def.
|
file |
diff |
annotate
|
| Tue, 03 Jul 2001 15:29:29 +0200 |
paulson |
new lemmas
|
file |
diff |
annotate
|
| Tue, 26 Jun 2001 17:05:10 +0200 |
paulson |
tidied
|
file |
diff |
annotate
|
| Wed, 13 Jun 2001 16:28:40 +0200 |
paulson |
a couple of new theorems
|
file |
diff |
annotate
|
| Sat, 09 Jun 2001 08:42:29 +0200 |
paulson |
new material from the Sylow proof
|
file |
diff |
annotate
|
| Sun, 20 May 2001 13:16:27 +0200 |
paulson |
new theorem dvd_mult_right
|
file |
diff |
annotate
|
| Tue, 23 Jan 2001 15:47:36 +0100 |
paulson |
the 0<n premise was unnecessary
|
file |
diff |
annotate
|
| Fri, 05 Jan 2001 14:28:10 +0100 |
nipkow |
Changed priority of dvd from 70 to 50 as befits a relation.
|
file |
diff |
annotate
|
| Wed, 06 Dec 2000 10:24:44 +0100 |
paulson |
deleting the assumption 0<c for div_mult2_eq and mod_mult2_eq and
|
file |
diff |
annotate
|
| Fri, 01 Dec 2000 11:03:31 +0100 |
paulson |
many new div and mod properties (borrowed from Integ/IntDiv)
|
file |
diff |
annotate
|
| Thu, 12 Oct 2000 12:15:23 +0200 |
paulson |
new theorems mod_eq_0_iff and mod_eqD; also new SD rule
|
file |
diff |
annotate
|
| Mon, 11 Sep 2000 13:03:11 +0200 |
paulson |
tidied
|
file |
diff |
annotate
|
| Thu, 07 Sep 2000 10:38:04 +0200 |
paulson |
strengthened dvd_mod & proofed dvd_mod_iff
|
file |
diff |
annotate
|
| Wed, 06 Sep 2000 08:04:41 +0200 |
nipkow |
less_induct -> nat_less_induct
|
file |
diff |
annotate
|
| Thu, 17 Aug 2000 12:02:01 +0200 |
paulson |
better rules for cancellation of common factors across comparisons
|
file |
diff |
annotate
|
| Thu, 22 Jun 2000 23:04:34 +0200 |
wenzelm |
bind_thm(s);
|
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:00:45 +0200 |
paulson |
tidied
|
file |
diff |
annotate
|
| Tue, 02 May 2000 18:56:39 +0200 |
paulson |
removed obsolete "evenness" proofs
|
file |
diff |
annotate
|
| Thu, 13 Apr 2000 10:30:28 +0200 |
nipkow |
made mod_less_divisor a simplification rule.
|
file |
diff |
annotate
|
| Thu, 09 Mar 2000 16:07:38 +0100 |
paulson |
mod_less, div_less are now default simprules
|
file |
diff |
annotate
|
| Tue, 07 Sep 1999 10:40:58 +0200 |
wenzelm |
isatool expandshort;
|
file |
diff |
annotate
|
| Mon, 06 Sep 1999 18:18:30 +0200 |
oheimb |
added theorem dvd_reduce
|
file |
diff |
annotate
|
| Mon, 26 Jul 1999 16:08:15 +0200 |
paulson |
new cancellation laws
|
file |
diff |
annotate
|
| Wed, 21 Jul 1999 15:26:17 +0200 |
paulson |
a stronger diff_less and no more le_diff_less
|
file |
diff |
annotate
|
| Mon, 19 Jul 1999 15:18:16 +0200 |
paulson |
new division laws taking advantage of (m div 0) = 0 and (m mod 0) = m
|
file |
diff |
annotate
|
| Thu, 15 Jul 1999 10:27:54 +0200 |
paulson |
qed_goal -> Goal
|
file |
diff |
annotate
|