Sat, 17 Dec 2016 15:22:13 +0100 |
haftmann |
streamlined computation rules for primality of numerals: no need to go via explicit conversion to nat
|
file |
diff |
annotate
|
Mon, 17 Oct 2016 17:33:07 +0200 |
nipkow |
setprod -> prod
|
file |
diff |
annotate
|
Fri, 16 Sep 2016 12:30:55 +0200 |
haftmann |
prefer abbreviation for trivial set conversion
|
file |
diff |
annotate
|
Fri, 16 Sep 2016 12:30:55 +0200 |
haftmann |
more lemmas
|
file |
diff |
annotate
|
Fri, 09 Sep 2016 15:12:40 +0200 |
nipkow |
msetsum -> set_mset, msetprod -> prod_mset
|
file |
diff |
annotate
|
Thu, 01 Sep 2016 11:53:07 +0200 |
Manuel Eberl |
Some facts about factorial and binomial coefficients
|
file |
diff |
annotate
|
Tue, 09 Aug 2016 12:30:31 +0200 |
eberlm |
Tuned primes
|
file |
diff |
annotate
|
Mon, 08 Aug 2016 17:47:51 +0200 |
eberlm |
is_prime -> prime
|
file |
diff |
annotate
|
Fri, 22 Jul 2016 15:39:27 +0200 |
eberlm |
Tuned primes
|
file |
diff |
annotate
|
Thu, 21 Jul 2016 10:06:04 +0200 |
eberlm |
Overhaul of prime/multiplicity/prime_factors
|
file |
diff |
annotate
|
Tue, 01 Mar 2016 10:36:19 +0100 |
haftmann |
tuned bootstrap order to provide type classes in a more sensible order
|
file |
diff |
annotate
|
Fri, 26 Feb 2016 22:15:09 +0100 |
Manuel Eberl |
Tuned Euclidean Rings/GCD rings
|
file |
diff |
annotate
|
Thu, 25 Feb 2016 16:49:00 +0000 |
paulson |
partial tidy-up of Sylow's theorem
|
file |
diff |
annotate
|
Wed, 17 Feb 2016 21:51:57 +0100 |
haftmann |
cleansed junk-producing interpretations for gcd/lcm on nat altogether
|
file |
diff |
annotate
|
Wed, 17 Feb 2016 21:51:57 +0100 |
haftmann |
dropped various legacy fact bindings
|
file |
diff |
annotate
|
Tue, 01 Dec 2015 14:09:10 +0000 |
paulson |
Removal of redundant lemmas (diff_less_iff, diff_le_iff) and of the abbreviation Exp. Addition of some new material.
|
file |
diff |
annotate
|
Mon, 27 Jul 2015 22:44:02 +0200 |
haftmann |
formal class for factorial (semi)rings
|
file |
diff |
annotate
|
Wed, 08 Jul 2015 14:01:41 +0200 |
haftmann |
avoid explicit definition of the relation of associated elements in a ring -- prefer explicit normalization instead
|
file |
diff |
annotate
|
Fri, 19 Jun 2015 21:41:33 +0200 |
wenzelm |
isabelle update_cartouches;
|
file |
diff |
annotate
|
Mon, 16 Mar 2015 15:30:00 +0000 |
paulson |
The factorial function, "fact", now has type "nat => 'a"
|
file |
diff |
annotate
|
Tue, 10 Mar 2015 16:12:35 +0000 |
paulson |
renaming HOL/Fact.thy -> Binomial.thy
|
file |
diff |
annotate
|
Tue, 10 Mar 2015 15:20:40 +0000 |
paulson |
Removal of the file HOL/Number_Theory/Binomial!! And class field_char_0 now declared in Int.thy
|
file |
diff |
annotate
|
Sun, 09 Nov 2014 10:03:18 +0100 |
haftmann |
reverted 1ebf0a1f12a4 after successful re-tuning of simp rules for divisibility
|
file |
diff |
annotate
|
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
|