| 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
|
| Sat, 28 Jun 2014 09:16:42 +0200 |
haftmann |
fact consolidation
|
file |
diff |
annotate
|
| Fri, 11 Apr 2014 22:53:33 +0200 |
nipkow |
made divide_pos_pos a simp rule
|
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
|
| 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
|
| Wed, 02 Apr 2014 18:35:01 +0200 |
hoelzl |
moved generic theorems from Complex_Analysis_Basic; fixed some theorem names
|
file |
diff |
annotate
|
| Wed, 26 Mar 2014 14:00:37 +0000 |
paulson |
Some useful lemmas
|
file |
diff |
annotate
|
| Mon, 24 Mar 2014 14:22:29 +0000 |
paulson |
rearranging some deriv theorems
|
file |
diff |
annotate
|
| Wed, 19 Mar 2014 21:59:31 +0100 |
wenzelm |
tuned proofs;
|
file |
diff |
annotate
|
| Wed, 19 Mar 2014 17:06:02 +0000 |
paulson |
Some rationalisation of basic lemmas
|
file |
diff |
annotate
|
| Mon, 17 Mar 2014 19:50:59 +0100 |
hoelzl |
update syntax of has_*derivative to infix 50; fixed proofs
|
file |
diff |
annotate
|
| Mon, 17 Mar 2014 19:12:52 +0100 |
hoelzl |
unify syntax for has_derivative and differentiable
|
file |
diff |
annotate
|
| Fri, 07 Mar 2014 15:52:56 +0000 |
paulson |
Some new proofs. Tidying up, esp to remove "apply rule".
|
file |
diff |
annotate
|
| Fri, 07 Mar 2014 12:35:06 +0000 |
paulson |
a few new lemmas
|
file |
diff |
annotate
|
| Fri, 01 Nov 2013 18:51:14 +0100 |
haftmann |
more simplification rules on unary and binary minus
|
file |
diff |
annotate
|
| Tue, 03 Sep 2013 22:04:23 +0200 |
wenzelm |
tuned proofs -- less guessing;
|
file |
diff |
annotate
|
| Tue, 03 Sep 2013 01:12:40 +0200 |
wenzelm |
tuned proofs -- clarified flow of facts wrt. calculation;
|
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: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
|
| 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 connected to HOL image; used to show intermediate value theorem
|
file |
diff |
annotate
|
| Fri, 22 Mar 2013 10:41:43 +0100 |
hoelzl |
move compact to the HOL image; prove compactness of real closed intervals; show that continuous functions attain supremum and infimum on compact sets
|
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
|
| Fri, 22 Mar 2013 10:41:43 +0100 |
hoelzl |
simplify proof of the Bolzano bisection lemma; use more meta-logic to state it; renamed lemma_Bolzano to Bolzano
|
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:12 +0100 |
hoelzl |
use filterlim in Lim and SEQ; tuned proofs
|
file |
diff |
annotate
|
| Mon, 03 Dec 2012 18:19:11 +0100 |
hoelzl |
conversion rules for at, at_left and at_right; applied to l'Hopital's rules.
|
file |
diff |
annotate
|
| Mon, 03 Dec 2012 18:19:09 +0100 |
hoelzl |
weakened assumptions for lhopital_right_0
|
file |
diff |
annotate
|
| Mon, 03 Dec 2012 18:19:08 +0100 |
hoelzl |
tuned proof
|
file |
diff |
annotate
|
| Mon, 03 Dec 2012 18:19:07 +0100 |
hoelzl |
add L'Hôpital's rule
|
file |
diff |
annotate
|
| Sun, 25 Mar 2012 20:15:39 +0200 |
huffman |
merged fork with new numeral representation (see NEWS)
|
file |
diff |
annotate
|
| Fri, 09 Dec 2011 11:31:13 +0100 |
noschinl |
more systematic lemma name
|
file |
diff |
annotate
|
| Sun, 20 Nov 2011 17:44:41 +0100 |
wenzelm |
'lemmas' / 'theorems' commands allow 'for' fixes and standardize the result before storing;
|
file |
diff |
annotate
|
| Fri, 28 Oct 2011 23:41:16 +0200 |
wenzelm |
tuned Named_Thms: proper binding;
|
file |
diff |
annotate
|
| Thu, 22 Sep 2011 14:12:16 -0700 |
huffman |
discontinued legacy theorem names from RealDef.thy
|
file |
diff |
annotate
|
| Tue, 13 Sep 2011 17:07:33 -0700 |
huffman |
tuned proofs
|
file |
diff |
annotate
|
| Mon, 12 Sep 2011 07:55:43 +0200 |
nipkow |
new fastforce replacing fastsimp - less confusing name
|
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:06:27 -0700 |
huffman |
remove redundant lemma lemma_DERIV_subst in favor of DERIV_cong
|
file |
diff |
annotate
|
| Fri, 19 Aug 2011 15:54:43 -0700 |
huffman |
Lim.thy: legacy theorems
|
file |
diff |
annotate
|
| Tue, 16 Aug 2011 09:31:23 -0700 |
huffman |
add simp rules for isCont
|
file |
diff |
annotate
|
| Mon, 15 Aug 2011 09:08:17 -0700 |
huffman |
simplify some proofs
|
file |
diff |
annotate
|
| Mon, 08 Aug 2011 16:57:37 -0700 |
huffman |
remove duplicate lemmas
|
file |
diff |
annotate
|
| Fri, 14 Jan 2011 15:44:47 +0100 |
wenzelm |
eliminated global prems;
|
file |
diff |
annotate
|
| Tue, 21 Dec 2010 15:00:59 +0100 |
hoelzl |
use DERIV_intros
|
file |
diff |
annotate
|
| Tue, 20 Jul 2010 06:35:29 +0200 |
haftmann |
robustified metis proof
|
file |
diff |
annotate
|
| Mon, 19 Jul 2010 20:19:03 +0200 |
haftmann |
diff_eq_diff_less_eq' replaces diff_eq_diff_less_eq
|
file |
diff |
annotate
|
| Mon, 19 Jul 2010 16:09:44 +0200 |
haftmann |
diff_minus subsumes diff_def
|
file |
diff |
annotate
|
| Sun, 09 May 2010 17:47:43 -0700 |
huffman |
avoid using real-specific versions of generic lemmas
|
file |
diff |
annotate
|
| Thu, 18 Feb 2010 14:21:44 -0800 |
huffman |
get rid of many duplicate simp rule warnings
|
file |
diff |
annotate
|
| Sat, 16 Jan 2010 17:15:28 +0100 |
haftmann |
dropped some old primrecs and some constdefs
|
file |
diff |
annotate
|
| Sun, 15 Nov 2009 00:34:21 +0100 |
wenzelm |
simplified bulky metis proofs;
|
file |
diff |
annotate
|
| Fri, 13 Nov 2009 15:38:45 +0100 |
wenzelm |
more "anti_sym" -> "antisym" (cf. a4179bf442d1);
|
file |
diff |
annotate
|