| 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:21 +0200 |
hoelzl |
import more stuff from the CLT proof; base the lborel measure on interval_measure; remove lebesgue measure
|
file |
diff |
annotate
|
| Wed, 18 Jun 2014 14:31:32 +0200 |
hoelzl |
filters are easier to define with INF on filters.
|
file |
diff |
annotate
|
| Wed, 18 Jun 2014 07:31:12 +0200 |
hoelzl |
moved lemmas from the proof of the Central Limit Theorem by Jeremy Avigad and Luke Serafin
|
file |
diff |
annotate
|
| Fri, 11 Apr 2014 22:53:33 +0200 |
nipkow |
made divide_pos_pos a simp rule
|
file |
diff |
annotate
|
| Fri, 11 Apr 2014 13:36:57 +0200 |
nipkow |
made mult_nonneg_nonneg a simp rule
|
file |
diff |
annotate
|
| Wed, 02 Apr 2014 18:35:07 +0200 |
hoelzl |
extend continuous_intros; remove continuous_on_intros and isCont_intros
|
file |
diff |
annotate
|
| Wed, 02 Apr 2014 16:45:31 +0100 |
paulson |
new theorem about zero limits
|
file |
diff |
annotate
|
| Mon, 31 Mar 2014 12:16:39 +0200 |
hoelzl |
add limits of power at top and bot
|
file |
diff |
annotate
|
| Wed, 12 Feb 2014 08:35:57 +0100 |
blanchet |
renamed 'nat_{case,rec}' to '{case,rec}_nat'
|
file |
diff |
annotate
|
| Wed, 25 Dec 2013 17:39:06 +0100 |
haftmann |
prefer more canonical names for lemmas on min/max
|
file |
diff |
annotate
|
| Tue, 05 Nov 2013 09:45:02 +0100 |
hoelzl |
move Lubs from HOL to HOL-Library (replaced by conditionally complete lattices)
|
file |
diff |
annotate
|
| Fri, 01 Nov 2013 18:51:14 +0100 |
haftmann |
more simplification rules on unary and binary minus
|
file |
diff |
annotate
|
| Fri, 13 Sep 2013 07:59:50 +0200 |
haftmann |
tuned proofs
|
file |
diff |
annotate
|
| Tue, 03 Sep 2013 22:04:23 +0200 |
wenzelm |
tuned proofs -- less guessing;
|
file |
diff |
annotate
|
| Thu, 30 May 2013 23:29:33 +0200 |
wenzelm |
tuned headers;
|
file |
diff |
annotate
|
| Tue, 09 Apr 2013 14:04:47 +0200 |
hoelzl |
move FrechetDeriv from the Library to HOL/Deriv; base DERIV on FDERIV and both derivatives allow a restricted support set; FDERIV is now an abbreviation of has_derivative
|
file |
diff |
annotate
|
| Tue, 09 Apr 2013 14:04:41 +0200 |
hoelzl |
remove the within-filter, replace "at" by "at _ within UNIV" (This allows to remove a couple of redundant lemmas)
|
file |
diff |
annotate
|
| Tue, 26 Mar 2013 12:21:01 +0100 |
hoelzl |
remove Metric_Spaces and move its content into Limits and Real_Vector_Spaces
|
file |
diff |
annotate
|
| Tue, 26 Mar 2013 12:21:00 +0100 |
hoelzl |
move theorems about compactness of real closed intervals, the intermediate value theorem, and lemmas about continuity of bijective functions from Deriv.thy to Limits.thy
|
file |
diff |
annotate
|
| Tue, 26 Mar 2013 12:20:58 +0100 |
hoelzl |
move SEQ.thy and Lim.thy to Limits.thy
|
file |
diff |
annotate
|
| Tue, 26 Mar 2013 12:20:57 +0100 |
hoelzl |
rename RealVector.thy to Real_Vector_Spaces.thy
|
file |
diff |
annotate
|
| Fri, 22 Mar 2013 10:41:43 +0100 |
hoelzl |
move continuous and continuous_on to the HOL image; isCont is an abbreviation for continuous (at x) (isCont is now restricted to a T2 space)
|
file |
diff |
annotate
|
| Fri, 22 Mar 2013 10:41:43 +0100 |
hoelzl |
generalize Bfun and Bseq to metric spaces; Bseq is an abbreviation for Bfun
|
file |
diff |
annotate
|
| Fri, 22 Mar 2013 10:41:43 +0100 |
hoelzl |
move metric_space to its own theory
|
file |
diff |
annotate
|
| Fri, 22 Mar 2013 10:41:42 +0100 |
hoelzl |
move topological_space to its own theory
|
file |
diff |
annotate
|
| Wed, 06 Mar 2013 16:56:21 +0100 |
hoelzl |
add tendsto_eq_intros: they add an additional rewriting step at the rhs of --->
|
file |
diff |
annotate
|
| Wed, 20 Feb 2013 12:04:42 +0100 |
hoelzl |
move auxiliary lemmas from Library/Extended_Reals to HOL image
|
file |
diff |
annotate
|
| Wed, 06 Feb 2013 17:57:21 +0100 |
hoelzl |
replace open_interval with the rule open_tendstoI; generalize Liminf/Limsup rules
|
file |
diff |
annotate
|
| Thu, 31 Jan 2013 11:31:27 +0100 |
hoelzl |
introduce order topology
|
file |
diff |
annotate
|