| 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
|
| 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
|
| Sat, 07 Mar 1998 16:29:29 +0100 |
nipkow |
Removed `addsplits [expand_if]'
|
file |
diff |
annotate
|
| Wed, 24 Dec 1997 10:02:30 +0100 |
paulson |
New Auto_tac (by Oheimb), and new syntax (without parens), and expandshort
|
file |
diff |
annotate
|
| Tue, 16 Dec 1997 17:58:03 +0100 |
wenzelm |
expandshort;
|
file |
diff |
annotate
|
| Thu, 11 Dec 1997 10:28:04 +0100 |
paulson |
Got rid of mod2_neq_0
|
file |
diff |
annotate
|
| Thu, 04 Dec 1997 09:05:39 +0100 |
nipkow |
Added thm mult_div_cancel
|
file |
diff |
annotate
|
| Wed, 03 Dec 1997 17:25:43 +0100 |
nipkow |
Replaced n ~= 0 by 0 < n
|
file |
diff |
annotate
|
| Mon, 03 Nov 1997 12:13:18 +0100 |
wenzelm |
isatool fixclasimp;
|
file |
diff |
annotate
|
| Sat, 01 Nov 1997 12:59:06 +0100 |
paulson |
New Blast_tac (and minor tidying...)
|
file |
diff |
annotate
|
| Fri, 17 Oct 1997 15:25:12 +0200 |
nipkow |
setloop split_tac -> addsplits
|
file |
diff |
annotate
|
| Mon, 29 Sep 1997 11:37:02 +0200 |
paulson |
Step_tac -> Safe_tac
|
file |
diff |
annotate
|
| Fri, 26 Sep 1997 10:21:14 +0200 |
paulson |
Minor tidying to use Clarify_tac, etc.
|
file |
diff |
annotate
|
| Fri, 04 Jul 1997 12:31:20 +0200 |
paulson |
Simplified the new proofs about division
|
file |
diff |
annotate
|
| Wed, 02 Jul 1997 11:59:10 +0200 |
nipkow |
Added the following lemmas tp Divides and a few others to Arith and NatDef:
|
file |
diff |
annotate
|
| Mon, 23 Jun 1997 10:42:03 +0200 |
paulson |
Ran expandshort
|
file |
diff |
annotate
|
| Fri, 06 Jun 1997 13:28:40 +0200 |
paulson |
Removed a few redundant additions of simprules or classical rules
|
file |
diff |
annotate
|
| Fri, 30 May 1997 15:15:57 +0200 |
paulson |
Moving div and mod from Arith to Divides
|
file |
diff |
annotate
|