src/HOL/Divides.thy
Thu, 16 Apr 2009 10:11:34 +0200 haftmann tightended specification of class semiring_div
Wed, 15 Apr 2009 15:30:37 +0200 haftmann more coherent developement in Divides.thy and IntDiv.thy
Wed, 01 Apr 2009 18:41:15 +0200 nipkow added nat_div_gt_0 [simp]
Wed, 01 Apr 2009 16:03:00 +0200 nipkow added strong_setprod_cong[cong] (in analogy with setsum)
Thu, 26 Mar 2009 20:08:55 +0100 wenzelm interpretation/interpret: prefixes are mandatory by default;
Sun, 22 Mar 2009 20:46:11 +0100 haftmann lemma nat_dvd_not_less moved here from Arith_Tools
Thu, 12 Mar 2009 23:01:25 +0100 haftmann merged
Thu, 12 Mar 2009 18:01:26 +0100 haftmann vague cleanup in arith proof tools setup: deleted dead code, more proper structures, clearer arrangement
Thu, 12 Mar 2009 15:31:26 +0100 nipkow added div lemmas
Wed, 04 Mar 2009 11:05:29 +0100 blanchet Merge.
Wed, 04 Mar 2009 10:45:52 +0100 blanchet Merge.
Tue, 03 Mar 2009 17:05:18 +0100 nipkow removed and renamed 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
Mon, 23 Feb 2009 13:55:36 -0800 huffman move lemma dvd_mod_imp_dvd into class semiring_div
Sun, 22 Feb 2009 11:30:41 +0100 nipkow added dvd_div_mult
Sat, 21 Feb 2009 20:52:30 +0100 nipkow Removed subsumed lemmas
Fri, 20 Feb 2009 20:50:49 +0100 nipkow removed subsumed lemmas
Wed, 18 Feb 2009 10:24:48 -0800 huffman generalize le_imp_power_dvd and power_le_dvd; move from Divides to Power
Tue, 17 Feb 2009 18:48:17 +0100 nipkow Cleaned up IntDiv and removed subsumed lemmas.
Sun, 15 Feb 2009 22:58:02 +0100 nipkow dvd and setprod lemmas
Wed, 28 Jan 2009 16:29:16 +0100 nipkow Replaced group_ and ring_simps by algebra_simps;
Fri, 16 Jan 2009 14:58:11 +0100 haftmann migrated class package to new locale implementation
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
Tue, 30 Dec 2008 11:10:01 +0100 ballarin Merged.
Thu, 11 Dec 2008 18:30:26 +0100 ballarin Conversion of HOL-Main and ZF to new locales.
Thu, 11 Dec 2008 08:56:02 +0100 nipkow codegen
Mon, 17 Nov 2008 17:00:55 +0100 haftmann tuned unfold_locales invocation
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 15:27:23 +0200 haftmann (re-)added simp rules for (_ + _) div/mod _
Fri, 18 Jul 2008 18:25:53 +0200 haftmann moved op dvd to theory Ring_and_Field; generalized a couple of lemmas
Fri, 11 Jul 2008 09:02:22 +0200 haftmann separate class dvd for divisibility predicate
Fri, 25 Apr 2008 15:30:33 +0200 krauss Merged theories about wellfoundedness into one: Wellfounded.thy
Mon, 17 Mar 2008 18:37:00 +0100 wenzelm removed duplicate lemmas;
Wed, 20 Feb 2008 14:52:34 +0100 haftmann using only an relation predicate to construct div and mod
Fri, 15 Feb 2008 16:09:12 +0100 haftmann <= and < on nat no longer depend on wellfounded relations
Wed, 13 Feb 2008 09:35:31 +0100 haftmann more abstract lemmas
Wed, 23 Jan 2008 22:57:09 +0100 wenzelm tuned proofs;
Tue, 22 Jan 2008 23:07:21 +0100 haftmann added class semiring_div
Fri, 07 Dec 2007 15:07:59 +0100 haftmann instantiation target rather than legacy instance
Tue, 23 Oct 2007 23:27:23 +0200 nipkow went back to >0
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
Tue, 16 Oct 2007 23:12:45 +0200 haftmann global class syntax
Fri, 12 Oct 2007 08:20:46 +0200 haftmann class div inherits from class times
Sat, 29 Sep 2007 08:58:51 +0200 haftmann proper syntax during class specification
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
less more (0) -100 -60 tip