Fri, 04 Jul 2014 20:18:47 +0200 | haftmann | reduced name variants for assoc and commute on plus and mult | file | diff | annotate |
Wed, 05 Feb 2014 17:06:11 +0000 | paulson | Number_Theory no longer introduces One_nat_def as a simprule. Tidied some proofs. | file | diff | annotate |
Fri, 24 Jan 2014 15:21:00 +0000 | paulson | Restored Suc rather than +1, and using Library/Binimial | file | diff | annotate |
Thu, 31 Oct 2013 11:44:20 +0100 | haftmann | generalised lemma | file | diff | annotate |
Sat, 15 Jun 2013 17:19:23 +0200 | haftmann | selection operator smallest_prime_beyond | file | diff | annotate |
Sun, 17 Feb 2013 21:29:30 +0100 | haftmann | Sieve of Eratosthenes | file | diff | annotate |