| Wed, 05 Nov 2014 19:43:17 +0100 |
nipkow |
reduced execution time
|
file |
diff |
annotate
|
| Sun, 02 Nov 2014 18:21:45 +0100 |
wenzelm |
modernized header uniformly as section;
|
file |
diff |
annotate
|
| Thu, 09 Oct 2014 22:43:48 +0200 |
haftmann |
more foundational definition for predicate even
|
file |
diff |
annotate
|
| Tue, 07 Oct 2014 23:29:43 +0200 |
wenzelm |
more bibtex entries;
|
file |
diff |
annotate
|
| 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
|
| Sun, 02 Feb 2014 19:15:25 +0000 |
paulson |
Number_Theory: prime is no longer overloaded, but only for nat. Automatic coercion to int enabled.
|
file |
diff |
annotate
|
| Sat, 01 Feb 2014 20:38:29 +0000 |
paulson |
Added material from Old_Number_Theory related to the Chinese Remainder Theorem
|
file |
diff |
annotate
|
| Fri, 31 Jan 2014 16:58:58 +0000 |
paulson |
Restoring some proofs from the equivalent file in Old_Number_Theory.
|
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 |
purely algebraic foundation for even/odd
|
file |
diff |
annotate
|
| Thu, 12 Sep 2013 15:08:07 -0700 |
huffman |
remove unneeded assumption from prime_dvd_power lemmas;
|
file |
diff |
annotate
|
| Sun, 25 Mar 2012 20:15:39 +0200 |
huffman |
merged fork with new numeral representation (see NEWS)
|
file |
diff |
annotate
|
| Sun, 20 Nov 2011 21:05:23 +0100 |
wenzelm |
eliminated obsolete "standard";
|
file |
diff |
annotate
|
| Sat, 10 Sep 2011 23:27:32 +0200 |
wenzelm |
misc tuning;
|
file |
diff |
annotate
|
| Wed, 07 Sep 2011 09:02:58 -0700 |
huffman |
avoid using legacy theorem names
|
file |
diff |
annotate
|
| Tue, 09 Nov 2010 13:59:37 +0000 |
paulson |
tidied using metis
|
file |
diff |
annotate
|
| Mon, 12 Jul 2010 08:58:13 +0200 |
haftmann |
dropped superfluous [code del]s
|
file |
diff |
annotate
|
| Mon, 28 Jun 2010 15:32:27 +0200 |
haftmann |
tuned theory text
|
file |
diff |
annotate
|
| Wed, 02 Jun 2010 16:24:14 +0200 |
haftmann |
absolute import -- must work with Main.thy / HOL-Proofs
|
file |
diff |
annotate
|
| Mon, 08 Mar 2010 09:38:58 +0100 |
haftmann |
transfer: avoid camel case
|
file |
diff |
annotate
|
| Fri, 04 Dec 2009 08:52:09 +0100 |
nipkow |
removed redundant lemma
|
file |
diff |
annotate
|
| Mon, 16 Nov 2009 17:22:10 +0000 |
webertj |
Fixed a typo in a comment.
|
file |
diff |
annotate
|
| Tue, 01 Sep 2009 15:39:33 +0200 |
haftmann |
some reorganization of number theory
|
file |
diff |
annotate
| base
|