src/HOL/Divides.thy
Wed, 15 Aug 2007 12:52:56 +0200 paulson ATP blacklisting is now in theory data, attribute noatp
Tue, 14 Aug 2007 23:04:27 +0200 huffman minimize imports
Tue, 24 Jul 2007 15:20:45 +0200 haftmann using class target
Tue, 10 Jul 2007 09:23:10 +0200 haftmann introduced (auxiliary) class dvd_mod for more convenient code generation
Thu, 31 May 2007 18:16:50 +0200 wenzelm removed dead code;
Sat, 19 May 2007 11:33:21 +0200 haftmann uniform module names for code generation
Thu, 17 May 2007 19:49:16 +0200 haftmann tuned
Thu, 10 May 2007 10:21:44 +0200 haftmann tuned
Sun, 06 May 2007 21:50:17 +0200 haftmann changed code generator invocation syntax
Thu, 26 Apr 2007 13:33:04 +0200 haftmann added lemmatas
Fri, 20 Apr 2007 11:21:42 +0200 haftmann Isar definitions are now added explicitly to code theorem table
Tue, 17 Apr 2007 00:30:44 +0200 wenzelm tuned proofs;
Tue, 20 Mar 2007 08:27:15 +0100 haftmann explizit "type" superclass
Wed, 07 Feb 2007 17:26:49 +0100 berghofe Adapted to changes in Transitive_Closure theory.
Wed, 27 Dec 2006 19:10:00 +0100 haftmann added OCaml code generation (without dictionaries)
Sat, 18 Nov 2006 00:20:15 +0100 haftmann div is now a class
Mon, 06 Nov 2006 16:28:31 +0100 haftmann code generator module naming improved
Wed, 20 Sep 2006 12:24:11 +0200 haftmann name shifts
Tue, 19 Sep 2006 15:21:43 +0200 haftmann explicit divmod algorithm for code generation
Wed, 30 Aug 2006 03:19:08 +0200 webertj lin_arith_prover: splitting reverted because of performance loss
Mon, 14 Aug 2006 13:46:06 +0200 haftmann simplified code generator setup
Sat, 29 Jul 2006 13:15:12 +0200 webertj lin_arith_prover splits certain operators (e.g. min, max, abs)
Wed, 26 Jul 2006 19:23:04 +0200 webertj linear arithmetic splits certain operators (e.g. min, max, abs)
Sat, 08 Jul 2006 12:54:30 +0200 wenzelm simprocs: no theory argument -- use simpset context instead;
Tue, 17 Jan 2006 16:36:57 +0100 haftmann substantial improvements in code generator
Fri, 18 Nov 2005 07:13:58 +0100 chaieb presburger method updated to deal better with mod and div, tweo lemmas added to Divides.thy
Fri, 11 Nov 2005 00:09:37 +0100 huffman add header
Fri, 23 Sep 2005 22:21:49 +0200 wenzelm Provers/cancel_sums.ML: Simplifier.inherit_bounds;
Tue, 20 Sep 2005 14:03:37 +0200 wenzelm tuned theory dependencies;
Tue, 16 Aug 2005 18:53:11 +0200 paulson more simprules now have names
Tue, 16 Aug 2005 15:36:28 +0200 paulson classical rules must have names for ATP integration
Wed, 13 Jul 2005 15:06:20 +0200 paulson generlization of some "nat" theorems
Thu, 07 Jul 2005 12:39:17 +0200 nipkow linear arithmetic now takes "&" in assumptions apart.
Fri, 14 Jan 2005 12:00:27 +0100 nipkow made diff_less a simp rule
Tue, 19 Oct 2004 18:18:45 +0200 paulson converted some induct_tac to induct
Wed, 18 Aug 2004 11:09:40 +0200 nipkow import -> imports
Mon, 16 Aug 2004 14:22:27 +0200 nipkow New theory header syntax.
Thu, 22 Apr 2004 10:43:06 +0200 paulson new lemmas
Fri, 05 Mar 2004 15:26:04 +0100 paulson some new results
Thu, 04 Mar 2004 12:06:07 +0100 paulson new material from Avigad, and simplified treatment of division by 0
Tue, 25 Nov 2003 10:37:03 +0100 paulson More refinements to Ring_and_Field and numerics. Conversion of Divides_lemmas
Fri, 26 Sep 2003 10:34:57 +0200 paulson misc tidying
Thu, 24 Jul 2003 18:23:00 +0200 paulson declarations moved from PreList.thy
Tue, 25 Mar 2003 09:56:01 +0100 berghofe New theorems split_div' and mod_div_equality'.
Fri, 23 Aug 2002 07:41:05 +0200 nipkow Added div+mod cancelling simproc
Fri, 31 May 2002 07:53:37 +0200 nipkow Now arith can deal with div/mod arbitrary nat numerals.
Wed, 15 May 2002 13:49:51 +0200 nipkow Divides.ML -> Divides_lemmas.ML
Sat, 01 Dec 2001 18:52:32 +0100 wenzelm renamed class "term" to "type" (actually "HOL.type");
Fri, 05 Jan 2001 14:28:10 +0100 nipkow Changed priority of dvd from 70 to 50 as befits a relation.
Fri, 01 Dec 2000 11:03:31 +0100 paulson many new div and mod properties (borrowed from Integ/IntDiv)
Fri, 13 Oct 2000 08:28:21 +0200 nipkow *** empty log message ***
Thu, 12 Oct 2000 18:38:23 +0200 nipkow *** empty log message ***
Wed, 24 May 2000 18:48:22 +0200 paulson installing plus_ac0 for nat
Sun, 21 May 2000 14:49:28 +0200 wenzelm replaced {{ }} by { };
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, 01 Jul 1999 10:33:50 +0200 paulson now div and mod are overloaded; dvd is polymorphic
Fri, 30 May 1997 15:15:57 +0200 paulson Moving div and mod from Arith to Divides
less more (0) tip