| Wed, 20 Jun 2007 19:49:14 +0200 |
huffman |
avoid using implicit prems in assumption
|
file |
diff |
annotate
|
| Wed, 20 Jun 2007 05:18:39 +0200 |
huffman |
change simp rules for of_nat to work like int did previously (reorient of_nat_Suc, remove of_nat_mult [simp]); preserve original variable names in legacy int theorems
|
file |
diff |
annotate
|
| Sun, 17 Jun 2007 18:47:03 +0200 |
nipkow |
tuned laws for cancellation in divisions for fields.
|
file |
diff |
annotate
|
| Thu, 07 Jun 2007 02:34:37 +0200 |
huffman |
tuned
|
file |
diff |
annotate
|
| Wed, 06 Jun 2007 18:32:05 +0200 |
huffman |
clean up proofs of exp_zero, sin_zero, cos_zero
|
file |
diff |
annotate
|
| Tue, 05 Jun 2007 16:31:10 +0200 |
chaieb |
lemma lemma_DERIV_subst moved to Deriv.thy
|
file |
diff |
annotate
|
| Tue, 05 Jun 2007 07:58:50 +0200 |
huffman |
remove simp attribute from lemma_STAR theorems
|
file |
diff |
annotate
|
| Tue, 05 Jun 2007 00:54:03 +0200 |
huffman |
add lemma exp_of_real
|
file |
diff |
annotate
|
| Thu, 31 May 2007 23:02:16 +0200 |
huffman |
replace (- 1) with -1
|
file |
diff |
annotate
|
| Thu, 31 May 2007 22:23:50 +0200 |
huffman |
simplify some proofs
|
file |
diff |
annotate
|
| Wed, 30 May 2007 02:41:26 +0200 |
huffman |
simplify names of locale interpretations
|
file |
diff |
annotate
|
| Mon, 28 May 2007 16:29:17 +0200 |
huffman |
generalized exp to work over any complete field; new proof of exp_add
|
file |
diff |
annotate
|
| Mon, 28 May 2007 03:45:41 +0200 |
huffman |
remove division_by_zero requirement from termdiffs lemmas; cleaned up some proofs
|
file |
diff |
annotate
|
| Fri, 25 May 2007 00:36:54 +0200 |
huffman |
simplify some proofs
|
file |
diff |
annotate
|
| Wed, 23 May 2007 07:00:18 +0200 |
huffman |
generalize powerseries and termdiffs lemmas using axclasses
|
file |
diff |
annotate
|
| Tue, 22 May 2007 07:29:49 +0200 |
huffman |
rename lemmas LIM_ident, isCont_ident, DERIV_ident
|
file |
diff |
annotate
|
| Mon, 21 May 2007 19:43:33 +0200 |
huffman |
new field_combine_numerals simproc, which uses fractions as coefficients
|
file |
diff |
annotate
|
| Sun, 20 May 2007 18:48:52 +0200 |
huffman |
define pi with THE instead of SOME; cleaned up
|
file |
diff |
annotate
|
| Sun, 20 May 2007 17:49:10 +0200 |
huffman |
add lemmas for sin,cos,tan of 30,45,60 degrees; cleaned up
|
file |
diff |
annotate
|
| Sun, 20 May 2007 10:13:06 +0200 |
huffman |
moved sqrt lemmas from Transcendental.thy to NthRoot.thy
|
file |
diff |
annotate
|
| Sun, 20 May 2007 09:50:56 +0200 |
huffman |
remove obsolete DERIV_ln lemmas
|
file |
diff |
annotate
|
| Sun, 20 May 2007 08:16:29 +0200 |
huffman |
add lemmas about inverse functions; cleaned up proof of polar_ex
|
file |
diff |
annotate
|
| Sun, 20 May 2007 05:27:45 +0200 |
huffman |
rearranged sections
|
file |
diff |
annotate
|
| Sat, 19 May 2007 04:51:03 +0200 |
huffman |
use THE instead of SOME
|
file |
diff |
annotate
|
| Fri, 18 May 2007 16:11:13 +0200 |
huffman |
use mult_strict_mono instead of real_mult_less_mono
|
file |
diff |
annotate
|
| Thu, 17 May 2007 21:51:32 +0200 |
huffman |
avoid using redundant lemmas from RealDef.thy
|
file |
diff |
annotate
|
| Tue, 15 May 2007 07:28:08 +0200 |
huffman |
clean up polar_Ex proofs; remove unnecessary lemmas
|
file |
diff |
annotate
|
| Tue, 15 May 2007 05:09:01 +0200 |
huffman |
remove simp attribute from various polar_Ex lemmas
|
file |
diff |
annotate
|
| Mon, 14 May 2007 23:25:16 +0200 |
huffman |
tuned proofs
|
file |
diff |
annotate
|
| Mon, 14 May 2007 23:09:54 +0200 |
huffman |
spelling: rename arcos -> arccos
|
file |
diff |
annotate
|
| Mon, 14 May 2007 18:04:52 +0200 |
huffman |
tuned proofs
|
file |
diff |
annotate
|
| Mon, 14 May 2007 09:16:47 +0200 |
huffman |
remove redundant lemmas
|
file |
diff |
annotate
|
| Sun, 13 May 2007 20:05:42 +0200 |
huffman |
define roots of negative reals so that many lemmas no longer require side conditions; simplification solves more goals than previously
|
file |
diff |
annotate
|
| Thu, 10 May 2007 04:06:56 +0200 |
huffman |
fix proofs
|
file |
diff |
annotate
|
| Tue, 17 Apr 2007 03:13:38 +0200 |
huffman |
lemma isCont_inv_fun is same as isCont_inverse_function
|
file |
diff |
annotate
|
| Tue, 17 Apr 2007 00:55:00 +0200 |
huffman |
moved root and sqrt lemmas from Transcendental.thy to NthRoot.thy
|
file |
diff |
annotate
|
| Fri, 13 Apr 2007 00:48:12 +0200 |
huffman |
new simp rule exp_ln; new standard proof of DERIV_exp_ln_one; changed imports
|
file |
diff |
annotate
|
| Fri, 13 Apr 2007 00:07:52 +0200 |
huffman |
moved nonstandard derivative stuff from Deriv.thy into new file HDeriv.thy
|
file |
diff |
annotate
|
| Sun, 08 Apr 2007 17:54:52 +0200 |
huffman |
remove redundant lemmas
|
file |
diff |
annotate
|
| Fri, 17 Nov 2006 02:20:03 +0100 |
wenzelm |
more robust syntax for definition/abbreviation/notation;
|
file |
diff |
annotate
|
| Sat, 04 Nov 2006 00:12:06 +0100 |
huffman |
moved DERIV stuff from Lim.thy to new Deriv.thy; cleaned up LIMSEQ_SEQ proofs
|
file |
diff |
annotate
|
| Fri, 13 Oct 2006 18:15:18 +0200 |
berghofe |
Adapted to changes in FixedPoint theory.
|
file |
diff |
annotate
|
| Thu, 05 Oct 2006 05:46:32 +0200 |
huffman |
reorganize and speed up termdiffs proofs
|
file |
diff |
annotate
|
| Tue, 03 Oct 2006 19:40:34 +0200 |
huffman |
rewrite proofs of powser_insidea and termdiffs_aux
|
file |
diff |
annotate
|
| Sun, 24 Sep 2006 05:49:50 +0200 |
huffman |
generalized types of sums, summable, and suminf
|
file |
diff |
annotate
|
| Sun, 24 Sep 2006 04:00:46 +0200 |
huffman |
remove extra dependencies
|
file |
diff |
annotate
|
| Sun, 24 Sep 2006 02:56:59 +0200 |
huffman |
move root and sqrt stuff from Transcendental to NthRoot
|
file |
diff |
annotate
|
| Fri, 22 Sep 2006 16:25:15 +0200 |
huffman |
define constants with THE instead of SOME
|
file |
diff |
annotate
|
| Sun, 17 Sep 2006 16:44:05 +0200 |
huffman |
generalize type of (NS)LIM to work on functions with vector space domain types
|
file |
diff |
annotate
|
| Sat, 16 Sep 2006 02:40:00 +0200 |
huffman |
generalized types of many constants to work over arbitrary vector spaces;
|
file |
diff |
annotate
|
| Tue, 12 Sep 2006 17:03:52 +0200 |
huffman |
realpow_divide -> power_divide
|
file |
diff |
annotate
|
| Wed, 30 Aug 2006 03:19:08 +0200 |
webertj |
lin_arith_prover: splitting reverted because of performance loss
|
file |
diff |
annotate
|
| Sun, 30 Jul 2006 05:53:10 +0200 |
webertj |
lin_arith_prover splits certain operators (e.g. min, max, abs)
|
file |
diff |
annotate
|
| Wed, 26 Jul 2006 19:23:04 +0200 |
webertj |
linear arithmetic splits certain operators (e.g. min, max, abs)
|
file |
diff |
annotate
|
| Fri, 02 Jun 2006 23:22:29 +0200 |
wenzelm |
misc cleanup;
|
file |
diff |
annotate
|
| Fri, 17 Mar 2006 10:04:27 +0100 |
ballarin |
Renamed setsum_mult to setsum_right_distrib.
|
file |
diff |
annotate
|
| Thu, 05 Jan 2006 22:29:55 +0100 |
wenzelm |
replaced swap by contrapos_np;
|
file |
diff |
annotate
|
| Fri, 09 Sep 2005 19:34:22 +0200 |
huffman |
starfun, starset, and other functions on NS types are now polymorphic;
|
file |
diff |
annotate
|
| Tue, 06 Sep 2005 23:16:48 +0200 |
huffman |
replace type hypreal with real star
|
file |
diff |
annotate
|
| Wed, 03 Aug 2005 14:48:50 +0200 |
avigad |
renamed exp_ge_add_one_self to exp_ge_add_one_self_aux
|
file |
diff |
annotate
|