src/HOL/Number_Theory/UniqueFactorization.thy
Thu, 11 Oct 2012 11:56:43 +0200 haftmann msetprod based directly on Multiset.fold;
Thu, 04 Oct 2012 23:19:02 +0200 haftmann simplified type of msetprod;
Thu, 04 Oct 2012 23:19:02 +0200 haftmann tuned proof
Thu, 04 Oct 2012 23:19:02 +0200 haftmann dropped duplicate facts; tuned syntax
Wed, 15 Aug 2012 14:26:42 +0200 nipkow fixed proof
Sat, 10 Sep 2011 23:27:32 +0200 wenzelm misc tuning;
Wed, 07 Sep 2011 09:02:58 -0700 huffman avoid using legacy theorem names
Sun, 13 Mar 2011 22:55:50 +0100 wenzelm tuned headers;
Thu, 13 Jan 2011 23:50:16 +0100 wenzelm eliminated global prems;
Wed, 29 Dec 2010 17:34:41 +0100 wenzelm explicit file specifications -- avoid secondary load path;
Tue, 09 Nov 2010 13:59:37 +0000 paulson tidied using metis
Mon, 13 Sep 2010 11:13:15 +0200 nipkow renamed lemmas: ext_iff -> fun_eq_iff, set_ext_iff -> set_eq_iff, set_ext -> set_eqI
Wed, 02 Jun 2010 15:35:14 +0200 haftmann msetprod_empty, msetprod_singleton
Thu, 13 May 2010 14:34:05 +0200 nipkow Multiset: renamed, added and tuned lemmas;
Mon, 08 Mar 2010 09:38:58 +0100 haftmann transfer: avoid camel case
Mon, 01 Mar 2010 13:40:23 +0100 haftmann replaced a couple of constsdefs by definitions (also some old primrecs by modern ones)
Mon, 08 Feb 2010 21:28:27 +0100 wenzelm modernized some syntax translations;
Fri, 22 Jan 2010 13:39:00 +0100 haftmann simplified proofs
Fri, 13 Nov 2009 14:14:04 +0100 nipkow renamed lemmas "anti_sym" -> "antisym"
Tue, 01 Sep 2009 15:39:33 +0200 haftmann some reorganization of number theory
less more (0) tip