2014-05-20 |
hoelzl |
add various lemmas
|
file |
diff |
annotate
|
2014-05-13 |
nipkow |
added lemmas
|
file |
diff |
annotate
|
2014-04-14 |
hoelzl |
added divide_nonneg_nonneg and co; made it a simp rule
|
file |
diff |
annotate
|
2014-04-12 |
nipkow |
made mult_pos_pos a simp rule
|
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-09 |
hoelzl |
generalize ln/log_powr; add log_base_powr/pow
|
file |
diff |
annotate
|
2014-04-09 |
hoelzl |
revert c1bbd3e22226, a14831ac3023, and 36489d77c484: divide_minus_left/right are again simp rules
|
file |
diff |
annotate
|
2014-04-03 |
paulson |
removing simprule status for divide_minus_left and divide_minus_right
|
file |
diff |
annotate
|
2014-04-03 |
hoelzl |
merged DERIV_intros, has_derivative_intros into derivative_intros
|
file |
diff |
annotate
|
2014-04-02 |
hoelzl |
extend continuous_intros; remove continuous_on_intros and isCont_intros
|
file |
diff |
annotate
|
2014-03-24 |
paulson |
rearranging some deriv theorems
|
file |
diff |
annotate
|
2014-03-19 |
paulson |
Some rationalisation of basic lemmas
|
file |
diff |
annotate
|
2014-03-19 |
hoelzl |
further renaming in Series
|
file |
diff |
annotate
|
2014-03-18 |
hoelzl |
cleanup Series: sorted according to typeclass hierarchy, use {..<_} instead of {0..<_}
|
file |
diff |
annotate
|
2014-03-17 |
hoelzl |
unify syntax for has_derivative and differentiable
|
file |
diff |
annotate
|
2014-03-16 |
huffman |
tuned proofs
|
file |
diff |
annotate
|
2014-03-02 |
wenzelm |
repaired document;
|
file |
diff |
annotate
|
2014-02-25 |
paulson |
More complex-related lemmas
|
file |
diff |
annotate
|
2014-02-24 |
paulson |
Lemmas about Reals, norm, etc., and cleaner variants of existing ones
|
file |
diff |
annotate
|
2014-02-12 |
blanchet |
adapted to 'xxx_{case,rec}' renaming, to new theorem names, and to new variable names in theorems
|
file |
diff |
annotate
|
2013-11-25 |
paulson |
tidied more proofs
|
file |
diff |
annotate
|
2013-11-24 |
paulson |
cleaned up more messy proofs
|
file |
diff |
annotate
|
2013-11-24 |
paulson |
cleaned up some messy proofs
|
file |
diff |
annotate
|
2013-11-19 |
haftmann |
eliminiated neg_numeral in favour of - (numeral _)
|
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-12 |
huffman |
generalize lemmas
|
file |
diff |
annotate
|
2013-08-18 |
wenzelm |
tuned proofs;
|
file |
diff |
annotate
|
2013-08-18 |
wenzelm |
more symbols;
|
file |
diff |
annotate
|
2013-08-13 |
wenzelm |
standardized symbols via "isabelle update_sub_sup", excluding src/Pure and src/Tools/WWW_Find;
|
file |
diff |
annotate
|
2013-05-25 |
noschinl |
add lemma
|
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 |
move Ln.thy and Log.thy to Transcendental.thy
|
file |
diff |
annotate
|
2013-03-22 |
hoelzl |
arcsin and arccos are continuous on {0 .. 1} (including the endpoints)
|
file |
diff |
annotate
|
2013-03-22 |
hoelzl |
move continuous_on_inv to HOL image (simplifies isCont_inverse_function)
|
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 |
clean up lemma_nest_unique and renamed to nested_sequence_unique
|
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 |
add filterlim rules for exp and ln to infinity
|
file |
diff |
annotate
|
2012-10-19 |
webertj |
Renamed {left,right}_distrib to distrib_{right,left}.
|
file |
diff |
annotate
|
2012-04-16 |
huffman |
tuned some proofs;
|
file |
diff |
annotate
|
2012-03-25 |
huffman |
merged fork with new numeral representation (see NEWS)
|
file |
diff |
annotate
|
2012-01-17 |
huffman |
factor-cancellation simprocs now call the full simplifier to prove that factors are non-zero
|
file |
diff |
annotate
|
2011-12-15 |
huffman |
tendsto lemmas for ln and powr
|
file |
diff |
annotate
|
2011-10-30 |
huffman |
removed ad-hoc simp rules sin_cos_eq[symmetric], minus_sin_cos_eq[symmetric], cos_sin_eq[symmetric]
|
file |
diff |
annotate
|
2011-10-30 |
huffman |
extend cancellation simproc patterns to cover terms like '- (2 * pi) < pi'
|
file |
diff |
annotate
|
2011-09-06 |
huffman |
simplify proof of tan_half, removing unused assumptions
|
file |
diff |
annotate
|
2011-09-06 |
huffman |
convert some proofs to Isar-style
|
file |
diff |
annotate
|
2011-09-06 |
huffman |
add lemmas about arctan;
|
file |
diff |
annotate
|
2011-09-06 |
huffman |
convert lemma cos_total to Isar-style proof
|
file |
diff |
annotate
|
2011-09-06 |
huffman |
convert lemma cos_is_zero to Isar-style
|
file |
diff |
annotate
|
2011-09-06 |
huffman |
convert lemma sin_gt_zero to Isar style;
|
file |
diff |
annotate
|
2011-09-05 |
huffman |
modify lemma sums_group, and shorten proofs that use it
|
file |
diff |
annotate
|
2011-09-05 |
huffman |
generalize some lemmas
|
file |
diff |
annotate
|
2011-09-05 |
huffman |
add lemmas cos_arctan and sin_arctan
|
file |
diff |
annotate
|
2011-09-04 |
huffman |
remove redundant lemmas about LIMSEQ
|
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 |
move sin_coeff and cos_coeff lemmas to Transcendental.thy; simplify some proofs
|
file |
diff |
annotate
|