| 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
|