src/HOL/Number_Theory/Factorial_Ring.thy
Mon, 05 Sep 2016 15:47:50 +0200 fleury add_mset constructor in multisets
Mon, 08 Aug 2016 17:47:51 +0200 eberlm is_prime -> prime
Mon, 25 Jul 2016 11:30:31 +0200 wenzelm merged
Fri, 22 Jul 2016 08:02:37 +0200 wenzelm tuned proofs -- avoid improper use of "this";
Fri, 22 Jul 2016 17:35:54 +0200 eberlm Removed redundant material related to primes
Thu, 21 Jul 2016 10:06:04 +0200 eberlm Overhaul of prime/multiplicity/prime_factors
Wed, 13 Jul 2016 15:46:52 +0200 eberlm Reformed factorial rings
Tue, 24 May 2016 18:46:51 +0200 eberlm Backed out changeset 8230358fab88
Tue, 24 May 2016 17:42:14 +0200 eberlm Deleted problematic code equation in Codegenerator_Test
Tue, 26 Apr 2016 22:44:31 +0200 wenzelm some uses of 'obtain' with structure statement;
Mon, 25 Apr 2016 16:09:26 +0200 wenzelm eliminated old 'def';
Thu, 03 Mar 2016 08:33:55 +0100 haftmann constructive formulation of factorization
Thu, 18 Feb 2016 17:53:09 +0100 haftmann more theorems
Wed, 17 Feb 2016 21:51:57 +0100 haftmann dropped various legacy fact bindings
Mon, 27 Jul 2015 22:44:02 +0200 haftmann formal class for factorial (semi)rings
less more (0) tip