| 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
|
| Thu, 01 Jul 1999 10:33:50 +0200 |
paulson |
now div and mod are overloaded; dvd is polymorphic
|
file |
diff |
annotate
|
| Sat, 09 Jan 1999 15:24:11 +0100 |
nipkow |
Refined arith tactic.
|
file |
diff |
annotate
|
| Fri, 27 Nov 1998 17:00:30 +0100 |
nipkow |
At last: linear arithmetic for nat!
|
file |
diff |
annotate
|
| Wed, 23 Sep 1998 10:12:01 +0200 |
paulson |
deleted needless parentheses
|
file |
diff |
annotate
|
| Fri, 18 Sep 1998 14:36:36 +0200 |
paulson |
tidying
|
file |
diff |
annotate
|
| Tue, 01 Sep 1998 15:03:43 +0200 |
paulson |
tidying; moved diff_less to Arith.ML
|
file |
diff |
annotate
|
| Thu, 20 Aug 1998 16:49:47 +0200 |
paulson |
tidied
|
file |
diff |
annotate
|
| Wed, 19 Aug 1998 10:26:37 +0200 |
paulson |
less_imp_diff_positive is redundant with new simprule zero_less_diff
|
file |
diff |
annotate
|
| Fri, 14 Aug 1998 12:03:01 +0200 |
paulson |
expandshort
|
file |
diff |
annotate
|
| Thu, 13 Aug 1998 18:14:26 +0200 |
paulson |
even more tidying of Goal commands
|
file |
diff |
annotate
|
| Thu, 06 Aug 1998 15:48:13 +0200 |
paulson |
even more tidying of Goal commands
|
file |
diff |
annotate
|
| Fri, 24 Jul 1998 13:03:20 +0200 |
berghofe |
Adapted to new datatype package.
|
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
|
| Tue, 21 Apr 1998 10:47:58 +0200 |
paulson |
Renamed mod_XXX_cancel to mod_XXX_self
|
file |
diff |
annotate
|
| Mon, 20 Apr 1998 10:38:30 +0200 |
paulson |
New laws for mod
|
file |
diff |
annotate
|
| Fri, 03 Apr 1998 11:20:41 +0200 |
paulson |
Tidied proofs by getting rid of case_tac
|
file |
diff |
annotate
|