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
|
Wed, 27 Jul 2005 11:28:18 +0200 |
paulson |
removed the dependence on abs_mult
|
file |
diff |
annotate
|
Wed, 13 Jul 2005 19:49:07 +0200 |
avigad |
Additions to the Real (and Hyperreal) libraries:
|
file |
diff |
annotate
|
Tue, 12 Jul 2005 17:56:03 +0200 |
avigad |
added lemmas to OrderedGroup.thy (reasoning about signs, absolute value, triangle inequalities)
|
file |
diff |
annotate
|
Fri, 01 Jul 2005 14:06:57 +0200 |
berghofe |
Simplified some proofs (thanks to strong_setsum_cong).
|
file |
diff |
annotate
|
Wed, 02 Mar 2005 12:06:15 +0100 |
nipkow |
another reorganization of setsums and intervals
|
file |
diff |
annotate
|
Wed, 23 Feb 2005 10:23:22 +0100 |
nipkow |
suminf -> \<Sum>
|
file |
diff |
annotate
|
Tue, 22 Feb 2005 13:05:47 +0100 |
paulson |
removed redundant lemmas and simprules
|
file |
diff |
annotate
|
Mon, 21 Feb 2005 19:23:46 +0100 |
nipkow |
more fine tuniung
|
file |
diff |
annotate
|
Mon, 21 Feb 2005 15:04:10 +0100 |
nipkow |
comprehensive cleanup, replacing sumr by setsum
|
file |
diff |
annotate
|
Fri, 18 Feb 2005 11:48:53 +0100 |
nipkow |
starting to get rid of sumr
|
file |
diff |
annotate
|
Tue, 01 Feb 2005 18:01:57 +0100 |
paulson |
the new subst tactic, by Lucas Dixon
|
file |
diff |
annotate
|
Tue, 07 Dec 2004 16:16:23 +0100 |
paulson |
made proofs more robust
|
file |
diff |
annotate
|
Tue, 19 Oct 2004 18:18:45 +0200 |
paulson |
converted some induct_tac to induct
|
file |
diff |
annotate
|
Tue, 12 Oct 2004 11:48:21 +0200 |
paulson |
tweaks concerned with poly bug-fixing
|
file |
diff |
annotate
|
Thu, 07 Oct 2004 15:42:30 +0200 |
paulson |
simplification tweaks for better arithmetic reasoning
|
file |
diff |
annotate
|
Tue, 05 Oct 2004 15:30:50 +0200 |
paulson |
new simprules for abs and for things like a/b<1
|
file |
diff |
annotate
|
Mon, 04 Oct 2004 15:28:03 +0200 |
paulson |
revised simprules for division
|
file |
diff |
annotate
|
Wed, 18 Aug 2004 11:09:40 +0200 |
nipkow |
import -> imports
|
file |
diff |
annotate
|
Mon, 16 Aug 2004 14:22:27 +0200 |
nipkow |
New theory header syntax.
|
file |
diff |
annotate
|
Thu, 29 Jul 2004 16:57:41 +0200 |
paulson |
removal of more iff-rules from RealDef.thy
|
file |
diff |
annotate
|
Thu, 29 Jul 2004 16:14:42 +0200 |
paulson |
removed some [iff] declarations from RealDef.thy, concerning inequalities
|
file |
diff |
annotate
|
Wed, 28 Jul 2004 16:25:40 +0200 |
paulson |
abs notation
|
file |
diff |
annotate
|
Wed, 28 Jul 2004 10:49:29 +0200 |
paulson |
conversion of Hyperreal/MacLaurin_lemmas to Isar script
|
file |
diff |
annotate
|
Mon, 26 Jul 2004 17:34:52 +0200 |
paulson |
converting Hyperreal/Transcendental to Isar script
|
file |
diff |
annotate
|
Thu, 01 Jul 2004 12:29:53 +0200 |
paulson |
new treatment of binary numerals
|
file |
diff |
annotate
|
Mon, 05 May 2003 18:23:40 +0200 |
paulson |
New material on integration, etc. Moving Hyperreal/ex
|
file |
diff |
annotate
|
Thu, 15 Nov 2001 16:12:49 +0100 |
paulson |
new theories from Jacques Fleuriot
|
file |
diff |
annotate
|