| Tue, 21 Jul 2009 14:08:58 +0200 | nipkow | Made dvd/gcd/lcm a complete lattice by introducing Gcd/GCD/Lcm/LCM | file | diff | annotate |
| Tue, 21 Jul 2009 11:01:07 +0200 | nipkow | Tests for executability of "prime" | file | diff | annotate |
| Fri, 17 Jul 2009 10:07:15 +0200 | berghofe | merged | file | diff | annotate |
| Tue, 14 Jul 2009 17:18:51 +0200 | berghofe | merged | file | diff | annotate |
| Fri, 10 Jul 2009 10:45:30 -0400 | avigad | Moved factorial lemmas from Binomial.thy to Fact.thy and merged. | file | diff | annotate |
| Wed, 15 Jul 2009 20:34:58 +0200 | nipkow | Made "prime" executable | file | diff | annotate |
| Mon, 13 Jul 2009 19:07:05 +0200 | berghofe | Tuned proof of lcm_1_iff_int, because metis produced enormous proof term. | file | diff | annotate |
| Sun, 12 Jul 2009 14:48:01 +0200 | nipkow | more gcd/lcm lemmas | file | diff | annotate |
| Sun, 12 Jul 2009 10:14:51 +0200 | nipkow | More about gcd/lcm, and some cleaning up | file | diff | annotate |
| Tue, 07 Jul 2009 17:39:51 +0200 | nipkow | renamed lemmas: nat_xyz/int_xyz -> xyz_nat/xyz_int | file | diff | annotate |
| Fri, 26 Jun 2009 19:44:39 +0200 | nipkow | lcm abs lemmas | file | diff | annotate |
| Fri, 26 Jun 2009 10:46:33 +0200 | nipkow | gcd abs lemmas | file | diff | annotate |
| Thu, 25 Jun 2009 07:34:12 +0200 | nipkow | Cleaned up GCD | file | diff | annotate |
| Tue, 23 Jun 2009 12:58:53 +0200 | nipkow | new lemmas | file | diff | annotate |
| Sun, 21 Jun 2009 23:04:37 +0200 | nipkow | new lemmas | file | diff | annotate |
| Sat, 20 Jun 2009 13:34:54 +0200 | nipkow | added lemmas; tuned | file | diff | annotate |
| Sat, 20 Jun 2009 01:53:39 +0200 | nipkow | new lemmas and tuning | file | diff | annotate |
| Thu, 18 Jun 2009 07:46:30 -0700 | huffman | more [code del] declarations | file | diff | annotate |
| Wed, 17 Jun 2009 16:55:01 -0700 | huffman | new GCD library, courtesy of Jeremy Avigad | file | diff | annotate |
| Fri, 27 Mar 2009 10:05:11 +0100 | haftmann | normalized imports | file | diff | annotate |
| Wed, 04 Mar 2009 11:05:29 +0100 | blanchet | Merge. | file | diff | annotate |
| Wed, 04 Mar 2009 10:45:52 +0100 | blanchet | Merge. | file | diff | annotate |
| Tue, 24 Feb 2009 11:12:58 -0800 | huffman | make more proofs work whether or not One_nat_def is a simp rule | file | diff | annotate |
| Sat, 21 Feb 2009 20:52:30 +0100 | nipkow | Removed subsumed lemmas | file | diff | annotate |
| Sat, 31 Jan 2009 09:04:16 +0100 | nipkow | added some simp rules | file | diff | annotate |
| Wed, 28 Jan 2009 11:03:42 +0100 | haftmann | Plain, Main form meeting points in import hierarchy | file | diff | annotate |
| Wed, 03 Dec 2008 15:58:44 +0100 | haftmann | made repository layout more coherent with logical distribution structure; stripped some $Id$s | file | diff | annotate | base |
| Fri, 08 Jul 2005 11:37:53 +0200 | nipkow | Used to be in Library/Primes | file | diff | annotate |