src/HOL/IntDiv.thy
Mon, 20 Jul 2009 08:32:07 +0200 haftmann merged
Tue, 14 Jul 2009 16:27:32 +0200 haftmann prefer code_inline over code_unfold; use code_unfold_post where appropriate
Wed, 15 Jul 2009 23:48:21 +0200 wenzelm more antiquotations;
Tue, 14 Jul 2009 10:54:04 +0200 haftmann code attributes use common underscore convention
Sun, 21 Jun 2009 23:04:37 +0200 nipkow new lemmas
Mon, 15 Jun 2009 21:29:04 -0700 huffman generalize lemmas dvd_mod and dvd_mod_iff to class semiring_div
Fri, 08 May 2009 09:48:07 +0200 haftmann modules numeral_simprocs, nat_numeral_simprocs; proper structures for numeral simprocs
Fri, 08 May 2009 08:00:11 +0200 haftmann moved int_factor_simprocs.ML to theory Int
Thu, 16 Apr 2009 14:02:11 +0200 haftmann tuned setups of CancelDivMod
Thu, 16 Apr 2009 10:11:34 +0200 haftmann tightended specification of class semiring_div
Sun, 22 Mar 2009 20:46:10 +0100 haftmann distributed contents of theory Arith_Tools to theories Int, IntDiv and NatBin accordingly
Fri, 13 Mar 2009 19:17:57 +0100 haftmann tuned ML code
Thu, 12 Mar 2009 18:01:26 +0100 haftmann vague cleanup in arith proof tools setup: deleted dead code, more proper structures, clearer arrangement
Fri, 06 Mar 2009 22:06:33 +0100 nipkow added lemma
Wed, 04 Mar 2009 11:05:29 +0100 blanchet Merge.
Wed, 04 Mar 2009 10:45:52 +0100 blanchet Merge.
Sun, 01 Mar 2009 12:01:57 +0100 nipkow removed redundant lemmas
Sun, 01 Mar 2009 10:24:57 +0100 nipkow added lemmas by Jeremy Avigad
Mon, 23 Feb 2009 16:25:52 -0800 huffman make proofs work whether or not One_nat_def is a simp rule; replace 1 with Suc 0 in the rhs of some simp rules
Sat, 21 Feb 2009 20:52:30 +0100 nipkow Removed subsumed lemmas
Sat, 21 Feb 2009 09:58:26 +0100 nipkow removed redundant thms
Fri, 20 Feb 2009 23:46:03 +0100 nipkow Removed redundant lemmas
Wed, 18 Feb 2009 15:01:53 -0800 huffman generalize int_dvd_cancel_factor simproc to idom class
Tue, 17 Feb 2009 10:52:55 -0800 huffman merged
Tue, 17 Feb 2009 07:13:29 -0800 huffman remove redundant simp attributes for zdvd rules
Tue, 17 Feb 2009 18:48:17 +0100 nipkow Cleaned up IntDiv and removed subsumed lemmas.
Mon, 16 Feb 2009 19:11:15 +0100 haftmann added pdivmod on int (for code generation)
Sat, 31 Jan 2009 09:04:16 +0100 nipkow added some simp rules
Wed, 28 Jan 2009 16:57:12 +0100 nipkow merged - resolving conflics
Wed, 28 Jan 2009 16:29:16 +0100 nipkow Replaced group_ and ring_simps by algebra_simps;
Wed, 28 Jan 2009 11:02:11 +0100 haftmann slightly adapted towards more uniformity with div/mod on nat
Thu, 08 Jan 2009 12:25:22 -0800 huffman remove type-specific proofs
Thu, 08 Jan 2009 09:12:29 -0800 huffman add class ring_div; generalize mod/diff/minus proofs for class ring_div
Thu, 08 Jan 2009 08:36:16 -0800 huffman generalize zmod_zmod_cancel -> mod_mod_cancel
Thu, 08 Jan 2009 08:24:08 -0800 huffman generalize some div/mod lemmas; remove type-specific proofs
Wed, 10 Dec 2008 07:52:54 -0800 huffman move nat_{div,mod}_distrib from NatBin to IntDiv, simplified proofs
Fri, 10 Oct 2008 06:45:53 +0200 haftmann `code func` now just `code`
Wed, 17 Sep 2008 21:27:08 +0200 wenzelm back to dynamic the_context(), because static @{theory} is invalidated if ML environment changes within the same code block;
Mon, 21 Jul 2008 13:36:44 +0200 chaieb Added theorems zmod_eq_dvd_iff and nat_mod_eq_iff previously in Pocklington.thy --- relevant for algebra
Fri, 18 Jul 2008 18:25:53 +0200 haftmann moved op dvd to theory Ring_and_Field; generalized a couple of lemmas
Wed, 02 Apr 2008 15:58:26 +0200 haftmann moved some code lemmas for Numerals here
Sat, 29 Mar 2008 19:14:00 +0100 wenzelm replaced 'ML_setup' by 'ML';
Wed, 20 Feb 2008 14:52:38 +0100 haftmann tuned structures in arith_data.ML
Sun, 17 Feb 2008 06:49:53 +0100 huffman New simpler representation of numerals, using Bit0 and Bit1 instead of BIT, B0, and B1
Fri, 25 Jan 2008 14:53:52 +0100 haftmann moved definition of power on ints to theory Int
Tue, 22 Jan 2008 23:07:21 +0100 haftmann added class semiring_div
Tue, 15 Jan 2008 16:19:23 +0100 haftmann joined theories IntDef, Numeral, IntArith to theory Int
Fri, 07 Dec 2007 15:07:59 +0100 haftmann instantiation target rather than legacy instance
Sun, 21 Oct 2007 14:53:44 +0200 nipkow Eliminated most of the neq0_conv occurrences. As a result, many
Sat, 20 Oct 2007 12:09:33 +0200 chaieb fixed proofs
Fri, 12 Oct 2007 08:20:46 +0200 haftmann class div inherits from class times
Tue, 18 Sep 2007 16:08:00 +0200 wenzelm simplified type int (eliminated IntInf.int, integer);
Thu, 30 Aug 2007 21:43:08 +0200 nipkow added lemma
Thu, 30 Aug 2007 05:01:38 +0200 huffman ported div/mod simprocs from HOL/ex/Binary.thy
Tue, 21 Aug 2007 20:51:10 +0200 huffman add lemma of_int_power
Wed, 15 Aug 2007 12:52:56 +0200 paulson ATP blacklisting is now in theory data, attribute noatp
Thu, 09 Aug 2007 15:52:45 +0200 haftmann tuned
Wed, 25 Jul 2007 18:10:28 +0200 nipkow Added lemmas
Tue, 24 Jul 2007 19:58:53 +0200 nipkow Added cancel simprocs for dvd on nat and int
Thu, 19 Jul 2007 21:47:38 +0200 haftmann added lemmas by Brian Huffman
less more (0) -60 tip