| Fri, 01 Jan 2010 16:34:51 +0100 |
nipkow |
removed FIXME
|
file |
diff |
annotate
|
| Tue, 08 Dec 2009 13:40:57 +0100 |
haftmann |
resorted code equations from "old" number theory version
|
file |
diff |
annotate
|
| Fri, 04 Dec 2009 08:52:09 +0100 |
nipkow |
removed redundant lemma
|
file |
diff |
annotate
|
| Fri, 13 Nov 2009 14:14:04 +0100 |
nipkow |
renamed lemmas "anti_sym" -> "antisym"
|
file |
diff |
annotate
|
| Thu, 29 Oct 2009 11:41:36 +0100 |
haftmann |
moved Nat_Transfer before Divides; distributed Nat_Transfer setup accordingly
|
file |
diff |
annotate
|
| Fri, 23 Oct 2009 18:59:24 +0200 |
blanchet |
continuation of Nitpick's integration into Isabelle;
|
file |
diff |
annotate
|
| Sat, 17 Oct 2009 14:43:18 +0200 |
wenzelm |
eliminated hard tabulators, guessing at each author's individual tab-width;
|
file |
diff |
annotate
|
| Tue, 06 Oct 2009 15:51:34 +0200 |
haftmann |
added syntactic Inf and Sup
|
file |
diff |
annotate
|
| Tue, 01 Sep 2009 15:39:33 +0200 |
haftmann |
some reorganization of number theory
|
file |
diff |
annotate
|
| Wed, 26 Aug 2009 19:54:01 +0200 |
nipkow |
got rid of complicated class finite_intvl_succ and defined "upto" directly on int, the only instance of the class.
|
file |
diff |
annotate
|
| 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
|