2015-03-31 |
haftmann |
given up separate type classes demanding `inverse 0 = 0`
|
file |
diff |
annotate
|
2015-03-05 |
paulson |
The function frac. Various lemmas about limits, series, the exp function, etc.
|
file |
diff |
annotate
|
2014-11-02 |
wenzelm |
modernized header uniformly as section;
|
file |
diff |
annotate
|
2014-10-20 |
hoelzl |
add tendsto_const and tendsto_ident_at as simp and intro rules
|
file |
diff |
annotate
|
2014-07-04 |
haftmann |
reduced name variants for assoc and commute on plus and mult
|
file |
diff |
annotate
|
2014-06-30 |
hoelzl |
import more stuff from the CLT proof; base the lborel measure on interval_measure; remove lebesgue measure
|
file |
diff |
annotate
|
2014-06-18 |
hoelzl |
filters are easier to define with INF on filters.
|
file |
diff |
annotate
|
2014-06-18 |
hoelzl |
moved lemmas from the proof of the Central Limit Theorem by Jeremy Avigad and Luke Serafin
|
file |
diff |
annotate
|
2014-04-11 |
nipkow |
made divide_pos_pos a simp rule
|
file |
diff |
annotate
|
2014-04-11 |
nipkow |
made mult_nonneg_nonneg a simp rule
|
file |
diff |
annotate
|
2014-04-02 |
hoelzl |
extend continuous_intros; remove continuous_on_intros and isCont_intros
|
file |
diff |
annotate
|
2014-04-02 |
paulson |
new theorem about zero limits
|
file |
diff |
annotate
|
2014-03-31 |
hoelzl |
add limits of power at top and bot
|
file |
diff |
annotate
|
2014-02-12 |
blanchet |
renamed 'nat_{case,rec}' to '{case,rec}_nat'
|
file |
diff |
annotate
|
2013-12-25 |
haftmann |
prefer more canonical names for lemmas on min/max
|
file |
diff |
annotate
|
2013-11-05 |
hoelzl |
move Lubs from HOL to HOL-Library (replaced by conditionally complete lattices)
|
file |
diff |
annotate
|
2013-11-01 |
haftmann |
more simplification rules on unary and binary minus
|
file |
diff |
annotate
|
2013-09-13 |
haftmann |
tuned proofs
|
file |
diff |
annotate
|
2013-09-03 |
wenzelm |
tuned proofs -- less guessing;
|
file |
diff |
annotate
|
2013-05-30 |
wenzelm |
tuned headers;
|
file |
diff |
annotate
|
2013-04-09 |
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
|
2013-04-09 |
hoelzl |
remove the within-filter, replace "at" by "at _ within UNIV" (This allows to remove a couple of redundant lemmas)
|
file |
diff |
annotate
|
2013-03-26 |
hoelzl |
remove Metric_Spaces and move its content into Limits and Real_Vector_Spaces
|
file |
diff |
annotate
|
2013-03-26 |
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
|
2013-03-26 |
hoelzl |
move SEQ.thy and Lim.thy to Limits.thy
|
file |
diff |
annotate
|
2013-03-26 |
hoelzl |
rename RealVector.thy to Real_Vector_Spaces.thy
|
file |
diff |
annotate
|
2013-03-22 |
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
|
2013-03-22 |
hoelzl |
generalize Bfun and Bseq to metric spaces; Bseq is an abbreviation for Bfun
|
file |
diff |
annotate
|
2013-03-22 |
hoelzl |
move metric_space to its own theory
|
file |
diff |
annotate
|
2013-03-22 |
hoelzl |
move topological_space to its own theory
|
file |
diff |
annotate
|
2013-03-06 |
hoelzl |
add tendsto_eq_intros: they add an additional rewriting step at the rhs of --->
|
file |
diff |
annotate
|
2013-02-20 |
hoelzl |
move auxiliary lemmas from Library/Extended_Reals to HOL image
|
file |
diff |
annotate
|
2013-02-06 |
hoelzl |
replace open_interval with the rule open_tendstoI; generalize Liminf/Limsup rules
|
file |
diff |
annotate
|
2013-01-31 |
hoelzl |
introduce order topology
|
file |
diff |
annotate
|
2013-01-14 |
hoelzl |
move eventually_Ball_finite to Limits
|
file |
diff |
annotate
|
2012-12-07 |
hoelzl |
add exponential and uniform distributions
|
file |
diff |
annotate
|
2012-12-04 |
hoelzl |
prove tendsto_power_div_exp_0
|
file |
diff |
annotate
|
2012-12-04 |
hoelzl |
add filterlim rules for eventually monotone bijective functions; mirror rules for at_top, at_bot; apply them to prove convergence of arctan at infinity and tan at pi/2
|
file |
diff |
annotate
|
2012-12-03 |
hoelzl |
use filterlim in Lim and SEQ; tuned proofs
|
file |
diff |
annotate
|
2012-12-03 |
hoelzl |
conversion rules for at, at_left and at_right; applied to l'Hopital's rules.
|
file |
diff |
annotate
|
2012-12-03 |
hoelzl |
add L'Hôpital's rule
|
file |
diff |
annotate
|
2012-12-03 |
hoelzl |
add filterlim rules for exp and ln to infinity
|
file |
diff |
annotate
|
2012-12-03 |
hoelzl |
add filterlim rules for inverse and at_infinity
|
file |
diff |
annotate
|
2012-12-03 |
hoelzl |
add filterlim rules for diverging multiplication and addition; move at_infinity to the HOL image
|
file |
diff |
annotate
|
2012-12-03 |
hoelzl |
add filterlim rules for unary minus and inverse
|
file |
diff |
annotate
|
2012-12-03 |
hoelzl |
rename filter_lim to filterlim to be consistent with filtermap
|
file |
diff |
annotate
|
2012-11-27 |
hoelzl |
introduce filter_lim as a generatlization of tendsto
|
file |
diff |
annotate
|
2012-10-12 |
wenzelm |
discontinued obsolete typedef (open) syntax;
|
file |
diff |
annotate
|
2012-04-12 |
wenzelm |
more standard method setup;
|
file |
diff |
annotate
|
2012-03-12 |
noschinl |
use eventually_elim method
|
file |
diff |
annotate
|
2012-03-12 |
noschinl |
add eventually_elim method
|
file |
diff |
annotate
|
2011-12-15 |
noschinl |
add lemmas about limits
|
file |
diff |
annotate
|
2011-10-28 |
wenzelm |
tuned Named_Thms: proper binding;
|
file |
diff |
annotate
|
2011-09-20 |
huffman |
add lemmas within_empty and tendsto_bot;
|
file |
diff |
annotate
|
2011-08-31 |
huffman |
convert to Isar-style proof
|
file |
diff |
annotate
|
2011-08-29 |
huffman |
move class perfect_space into RealVector.thy;
|
file |
diff |
annotate
|
2011-08-28 |
huffman |
discontinue many legacy theorems about LIM and LIMSEQ, in favor of tendsto theorems
|
file |
diff |
annotate
|
2011-08-20 |
huffman |
redefine constant 'trivial_limit' as an abbreviation
|
file |
diff |
annotate
|
2011-08-18 |
huffman |
remove bounded_(bi)linear locale interpretations, to avoid duplicating so many lemmas
|
file |
diff |
annotate
|
2011-08-17 |
huffman |
add lemma tendsto_compose_eventually; use it to shorten some proofs
|
file |
diff |
annotate
|