| Tue, 21 Apr 2015 17:19:00 +0100 |
paulson |
New material, mostly about limits. Consolidation.
|
file |
diff |
annotate
|
| Tue, 31 Mar 2015 21:54:32 +0200 |
haftmann |
given up separate type classes demanding `inverse 0 = 0`
|
file |
diff |
annotate
|
| Tue, 31 Mar 2015 15:00:03 +0100 |
paulson |
New material and binomial fix
|
file |
diff |
annotate
|
| Tue, 17 Mar 2015 15:11:25 +0000 |
paulson |
more general type class for factorial. Now allows code generation (?)
|
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
| base
|
| Wed, 26 Jul 2006 19:23:04 +0200 |
webertj |
linear arithmetic splits certain operators (e.g. min, max, abs)
|
file |
diff |
annotate
|
| Fri, 17 Mar 2006 10:04:27 +0100 |
ballarin |
Renamed setsum_mult to setsum_right_distrib.
|
file |
diff |
annotate
|
| Tue, 20 Sep 2005 14:03:37 +0200 |
wenzelm |
tuned theory dependencies;
|
file |
diff |
annotate
|
| Thu, 07 Jul 2005 12:36:56 +0200 |
nipkow |
Used to be part of Finite_Set (or was it SetInterval?)
|
file |
diff |
annotate
|