| Sat, 05 Jul 2014 11:01:53 +0200 |
haftmann |
prefer ac_simps collections over separate name bindings for add and mult
|
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
|
| Mon, 30 Jun 2014 15:45:25 +0200 |
hoelzl |
more equalities of topological filters; strengthen dependent_nat_choice; tuned a couple of proofs
|
file |
diff |
annotate
|
| Mon, 30 Jun 2014 15:45:21 +0200 |
hoelzl |
import more stuff from the CLT proof; base the lborel measure on interval_measure; remove lebesgue measure
|
file |
diff |
annotate
|
| Sat, 28 Jun 2014 09:16:42 +0200 |
haftmann |
fact consolidation
|
file |
diff |
annotate
|
| Fri, 30 May 2014 14:55:10 +0200 |
hoelzl |
introduce more powerful reindexing rules for big operators
|
file |
diff |
annotate
|
| Thu, 29 May 2014 14:39:19 +0100 |
paulson |
New theorems to enable the simplification of certain functions when applied to specific natural number constants (such as 4)
|
file |
diff |
annotate
|
| Tue, 13 May 2014 11:35:47 +0200 |
hoelzl |
clean up Lebesgue integration
|
file |
diff |
annotate
|
| Wed, 09 Apr 2014 09:37:48 +0200 |
hoelzl |
field_simps: better support for negation and division, and power
|
file |
diff |
annotate
|
| Mon, 31 Mar 2014 12:16:35 +0200 |
hoelzl |
add rules about infinity of intervals
|
file |
diff |
annotate
|
| Fri, 21 Mar 2014 15:36:00 +0000 |
paulson |
a few new lemmas and generalisations of old ones
|
file |
diff |
annotate
|
| Wed, 19 Mar 2014 14:54:45 +0000 |
paulson |
New complex analysis material
|
file |
diff |
annotate
|
| Tue, 18 Mar 2014 16:29:32 +0100 |
hoelzl |
fix HOL-NSA; move lemmas
|
file |
diff |
annotate
|
| Tue, 18 Mar 2014 15:53:48 +0100 |
hoelzl |
cleanup Series: sorted according to typeclass hierarchy, use {..<_} instead of {0..<_}
|
file |
diff |
annotate
|
| Mon, 24 Feb 2014 16:56:04 +0000 |
paulson |
Lemmas about Reals, norm, etc., and cleaner variants of existing ones
|
file |
diff |
annotate
|