src/HOL/Divides.ML
Tue, 23 May 2000 18:06:22 +0200 paulson added type constraint ::nat because 0 is now overloaded
Fri, 12 May 2000 15:00:45 +0200 paulson tidied
Tue, 02 May 2000 18:56:39 +0200 paulson removed obsolete "evenness" proofs
Thu, 13 Apr 2000 10:30:28 +0200 nipkow made mod_less_divisor a simplification rule.
Thu, 09 Mar 2000 16:07:38 +0100 paulson mod_less, div_less are now default simprules
Tue, 07 Sep 1999 10:40:58 +0200 wenzelm isatool expandshort;
Mon, 06 Sep 1999 18:18:30 +0200 oheimb added theorem dvd_reduce
Mon, 26 Jul 1999 16:08:15 +0200 paulson new cancellation laws
Wed, 21 Jul 1999 15:26:17 +0200 paulson a stronger diff_less and no more le_diff_less
Mon, 19 Jul 1999 15:18:16 +0200 paulson new division laws taking advantage of (m div 0) = 0 and (m mod 0) = m
Thu, 15 Jul 1999 10:27:54 +0200 paulson qed_goal -> Goal
Thu, 01 Jul 1999 10:33:50 +0200 paulson now div and mod are overloaded; dvd is polymorphic
Sat, 09 Jan 1999 15:24:11 +0100 nipkow Refined arith tactic.
Fri, 27 Nov 1998 17:00:30 +0100 nipkow At last: linear arithmetic for nat!
Wed, 23 Sep 1998 10:12:01 +0200 paulson deleted needless parentheses
Fri, 18 Sep 1998 14:36:36 +0200 paulson tidying
Tue, 01 Sep 1998 15:03:43 +0200 paulson tidying; moved diff_less to Arith.ML
Thu, 20 Aug 1998 16:49:47 +0200 paulson tidied
Wed, 19 Aug 1998 10:26:37 +0200 paulson less_imp_diff_positive is redundant with new simprule zero_less_diff
Fri, 14 Aug 1998 12:03:01 +0200 paulson expandshort
Thu, 13 Aug 1998 18:14:26 +0200 paulson even more tidying of Goal commands
Thu, 06 Aug 1998 15:48:13 +0200 paulson even more tidying of Goal commands
Fri, 24 Jul 1998 13:03:20 +0200 berghofe Adapted to new datatype package.
Wed, 15 Jul 1998 10:15:13 +0200 paulson Removal of leading "\!\!..." from most Goal commands
Mon, 22 Jun 1998 17:26:46 +0200 wenzelm isatool fixgoal;
Tue, 21 Apr 1998 10:47:58 +0200 paulson Renamed mod_XXX_cancel to mod_XXX_self
Mon, 20 Apr 1998 10:38:30 +0200 paulson New laws for mod
Fri, 03 Apr 1998 11:20:41 +0200 paulson Tidied proofs by getting rid of case_tac
Sat, 07 Mar 1998 16:29:29 +0100 nipkow Removed `addsplits [expand_if]'
Wed, 24 Dec 1997 10:02:30 +0100 paulson New Auto_tac (by Oheimb), and new syntax (without parens), and expandshort
Tue, 16 Dec 1997 17:58:03 +0100 wenzelm expandshort;
Thu, 11 Dec 1997 10:28:04 +0100 paulson Got rid of mod2_neq_0
Thu, 04 Dec 1997 09:05:39 +0100 nipkow Added thm mult_div_cancel
Wed, 03 Dec 1997 17:25:43 +0100 nipkow Replaced n ~= 0 by 0 < n
Mon, 03 Nov 1997 12:13:18 +0100 wenzelm isatool fixclasimp;
Sat, 01 Nov 1997 12:59:06 +0100 paulson New Blast_tac (and minor tidying...)
Fri, 17 Oct 1997 15:25:12 +0200 nipkow setloop split_tac -> addsplits
Mon, 29 Sep 1997 11:37:02 +0200 paulson Step_tac -> Safe_tac
Fri, 26 Sep 1997 10:21:14 +0200 paulson Minor tidying to use Clarify_tac, etc.
Fri, 04 Jul 1997 12:31:20 +0200 paulson Simplified the new proofs about division
Wed, 02 Jul 1997 11:59:10 +0200 nipkow Added the following lemmas tp Divides and a few others to Arith and NatDef:
Mon, 23 Jun 1997 10:42:03 +0200 paulson Ran expandshort
Fri, 06 Jun 1997 13:28:40 +0200 paulson Removed a few redundant additions of simprules or classical rules
Fri, 30 May 1997 15:15:57 +0200 paulson Moving div and mod from Arith to Divides
less more (0) tip