| Mon, 14 Apr 2014 13:08:17 +0200 |
hoelzl |
added divide_nonneg_nonneg and co; made it a simp rule
|
file |
diff |
annotate
|
| Sat, 12 Apr 2014 17:26:27 +0200 |
nipkow |
made mult_pos_pos a simp rule
|
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, 09 Apr 2014 13:15:21 +0200 |
hoelzl |
generalize ln/log_powr; add log_base_powr/pow
|
file |
diff |
annotate
|
| Wed, 09 Apr 2014 09:37:47 +0200 |
hoelzl |
revert c1bbd3e22226, a14831ac3023, and 36489d77c484: divide_minus_left/right are again simp rules
|
file |
diff |
annotate
|
| Thu, 03 Apr 2014 23:51:52 +0100 |
paulson |
removing simprule status for divide_minus_left and divide_minus_right
|
file |
diff |
annotate
|
| Thu, 03 Apr 2014 17:56:08 +0200 |
hoelzl |
merged DERIV_intros, has_derivative_intros into derivative_intros
|
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
|
| Mon, 24 Mar 2014 14:22:29 +0000 |
paulson |
rearranging some deriv theorems
|
file |
diff |
annotate
|
| Wed, 19 Mar 2014 17:06:02 +0000 |
paulson |
Some rationalisation of basic lemmas
|
file |
diff |
annotate
|
| Wed, 19 Mar 2014 15:34:57 +0100 |
hoelzl |
further renaming in Series
|
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, 17 Mar 2014 19:12:52 +0100 |
hoelzl |
unify syntax for has_derivative and differentiable
|
file |
diff |
annotate
|
| Sun, 16 Mar 2014 13:34:35 -0700 |
huffman |
tuned proofs
|
file |
diff |
annotate
|
| Sun, 02 Mar 2014 18:11:30 +0100 |
wenzelm |
repaired document;
|
file |
diff |
annotate
|
| Tue, 25 Feb 2014 16:17:20 +0000 |
paulson |
More complex-related lemmas
|
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
|
| Wed, 12 Feb 2014 08:37:06 +0100 |
blanchet |
adapted to 'xxx_{case,rec}' renaming, to new theorem names, and to new variable names in theorems
|
file |
diff |
annotate
|
| Mon, 25 Nov 2013 00:02:39 +0000 |
paulson |
tidied more proofs
|
file |
diff |
annotate
|
| Sun, 24 Nov 2013 18:37:25 +0000 |
paulson |
cleaned up more messy proofs
|
file |
diff |
annotate
|
| Sun, 24 Nov 2013 13:06:22 +0000 |
paulson |
cleaned up some messy proofs
|
file |
diff |
annotate
|
| Tue, 19 Nov 2013 10:05:53 +0100 |
haftmann |
eliminiated neg_numeral in favour of - (numeral _)
|
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
|
| Thu, 12 Sep 2013 15:08:46 -0700 |
huffman |
generalize lemmas
|
file |
diff |
annotate
|
| Sun, 18 Aug 2013 22:44:39 +0200 |
wenzelm |
tuned proofs;
|
file |
diff |
annotate
|
| Sun, 18 Aug 2013 18:49:45 +0200 |
wenzelm |
more symbols;
|
file |
diff |
annotate
|
| Tue, 13 Aug 2013 16:25:47 +0200 |
wenzelm |
standardized symbols via "isabelle update_sub_sup", excluding src/Pure and src/Tools/WWW_Find;
|
file |
diff |
annotate
|
| Sat, 25 May 2013 13:59:08 +0200 |
noschinl |
add lemma
|
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:20:59 +0100 |
hoelzl |
move Ln.thy and Log.thy to Transcendental.thy
|
file |
diff |
annotate
|
| Fri, 22 Mar 2013 10:41:43 +0100 |
hoelzl |
arcsin and arccos are continuous on {0 .. 1} (including the endpoints)
|
file |
diff |
annotate
|
| Fri, 22 Mar 2013 10:41:43 +0100 |
hoelzl |
move continuous_on_inv to HOL image (simplifies isCont_inverse_function)
|
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 |
clean up lemma_nest_unique and renamed to nested_sequence_unique
|
file |
diff |
annotate
|
| Tue, 04 Dec 2012 18:00:37 +0100 |
hoelzl |
prove tendsto_power_div_exp_0
|
file |
diff |
annotate
|
| Tue, 04 Dec 2012 18:00:31 +0100 |
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
|
| Mon, 03 Dec 2012 18:19:05 +0100 |
hoelzl |
add filterlim rules for exp and ln to infinity
|
file |
diff |
annotate
|
| Fri, 19 Oct 2012 15:12:52 +0200 |
webertj |
Renamed {left,right}_distrib to distrib_{right,left}.
|
file |
diff |
annotate
|
| Mon, 16 Apr 2012 11:24:57 +0200 |
huffman |
tuned some proofs;
|
file |
diff |
annotate
|
| Sun, 25 Mar 2012 20:15:39 +0200 |
huffman |
merged fork with new numeral representation (see NEWS)
|
file |
diff |
annotate
|
| Tue, 17 Jan 2012 16:30:54 +0100 |
huffman |
factor-cancellation simprocs now call the full simplifier to prove that factors are non-zero
|
file |
diff |
annotate
|
| Thu, 15 Dec 2011 17:21:29 +0100 |
huffman |
tendsto lemmas for ln and powr
|
file |
diff |
annotate
|
| Sun, 30 Oct 2011 09:42:13 +0100 |
huffman |
removed ad-hoc simp rules sin_cos_eq[symmetric], minus_sin_cos_eq[symmetric], cos_sin_eq[symmetric]
|
file |
diff |
annotate
|
| Sun, 30 Oct 2011 09:07:02 +0100 |
huffman |
extend cancellation simproc patterns to cover terms like '- (2 * pi) < pi'
|
file |
diff |
annotate
|
| Tue, 06 Sep 2011 10:30:00 -0700 |
huffman |
simplify proof of tan_half, removing unused assumptions
|
file |
diff |
annotate
|
| Tue, 06 Sep 2011 09:56:09 -0700 |
huffman |
convert some proofs to Isar-style
|
file |
diff |
annotate
|
| Mon, 05 Sep 2011 22:30:25 -0700 |
huffman |
add lemmas about arctan;
|
file |
diff |
annotate
|
| Mon, 05 Sep 2011 18:06:02 -0700 |
huffman |
convert lemma cos_total to Isar-style proof
|
file |
diff |
annotate
|
| Mon, 05 Sep 2011 17:45:37 -0700 |
huffman |
convert lemma cos_is_zero to Isar-style
|
file |
diff |
annotate
|
| Mon, 05 Sep 2011 17:00:56 -0700 |
huffman |
convert lemma sin_gt_zero to Isar style;
|
file |
diff |
annotate
|
| Mon, 05 Sep 2011 16:26:57 -0700 |
huffman |
modify lemma sums_group, and shorten proofs that use it
|
file |
diff |
annotate
|
| Mon, 05 Sep 2011 16:07:40 -0700 |
huffman |
generalize some lemmas
|
file |
diff |
annotate
|
| Mon, 05 Sep 2011 12:19:04 -0700 |
huffman |
add lemmas cos_arctan and sin_arctan
|
file |
diff |
annotate
|
| Sun, 04 Sep 2011 09:49:45 -0700 |
huffman |
remove redundant lemmas about LIMSEQ
|
file |
diff |
annotate
|
| Sun, 28 Aug 2011 09:20:12 -0700 |
huffman |
discontinue many legacy theorems about LIM and LIMSEQ, in favor of tendsto theorems
|
file |
diff |
annotate
|
| Fri, 19 Aug 2011 18:42:41 -0700 |
huffman |
move sin_coeff and cos_coeff lemmas to Transcendental.thy; simplify some proofs
|
file |
diff |
annotate
|
| Fri, 19 Aug 2011 18:08:05 -0700 |
huffman |
remove unused lemma DERIV_sin_add
|
file |
diff |
annotate
|
| Fri, 19 Aug 2011 18:06:27 -0700 |
huffman |
remove redundant lemma lemma_DERIV_subst in favor of DERIV_cong
|
file |
diff |
annotate
|