| Fri, 10 Oct 2008 06:45:53 +0200 |
haftmann |
`code func` now just `code`
|
file |
diff |
annotate
|
| Wed, 02 Jul 2008 07:11:57 +0200 |
haftmann |
cleaned up some code generator configuration
|
file |
diff |
annotate
|
| Wed, 20 Jun 2007 19:49:14 +0200 |
huffman |
avoid using implicit prems in assumption
|
file |
diff |
annotate
|
| Wed, 30 May 2007 02:41:26 +0200 |
huffman |
simplify names of locale interpretations
|
file |
diff |
annotate
|
| Tue, 29 May 2007 17:36:35 +0200 |
huffman |
add isUCont lemmas
|
file |
diff |
annotate
|
| Tue, 22 May 2007 19:47:55 +0200 |
huffman |
generalize uniqueness of limits to class real_normed_algebra_1
|
file |
diff |
annotate
|
| Tue, 22 May 2007 07:29:49 +0200 |
huffman |
rename lemmas LIM_ident, isCont_ident, DERIV_ident
|
file |
diff |
annotate
|
| Sun, 20 May 2007 03:18:50 +0200 |
huffman |
add lemmas LIM_compose2, isCont_LIM_compose2
|
file |
diff |
annotate
|
| Sat, 19 May 2007 04:52:24 +0200 |
huffman |
remove dependence on Hilbert_Choice.thy
|
file |
diff |
annotate
|
| Thu, 12 Apr 2007 03:37:30 +0200 |
huffman |
moved nonstandard limit stuff from Lim.thy into new theory HLim.thy
|
file |
diff |
annotate
|
| Thu, 12 Apr 2007 01:53:02 +0200 |
huffman |
new standard proof of lemma LIM_inverse
|
file |
diff |
annotate
|
| Wed, 11 Apr 2007 04:13:06 +0200 |
huffman |
moved nonstandard stuff from SEQ.thy into new file HSEQ.thy
|
file |
diff |
annotate
|
| Tue, 10 Apr 2007 22:01:19 +0200 |
huffman |
new LIM/isCont lemmas for abs, of_real, and power
|
file |
diff |
annotate
|
| Sun, 08 Apr 2007 17:54:52 +0200 |
huffman |
remove redundant lemmas
|
file |
diff |
annotate
|
| Wed, 14 Mar 2007 21:40:28 +0100 |
huffman |
move bounded (bi)linear operator locales from Lim.thy to RealVector.thy
|
file |
diff |
annotate
|
| Wed, 13 Dec 2006 00:07:13 +0100 |
huffman |
generalized some lemmas; removed redundant lemmas; cleaned up some proofs
|
file |
diff |
annotate
|
| Tue, 12 Dec 2006 07:13:06 +0100 |
huffman |
cleaned up; generalized some proofs
|
file |
diff |
annotate
|
| Sun, 10 Dec 2006 07:12:26 +0100 |
nipkow |
Modified lattice locale
|
file |
diff |
annotate
|
| Fri, 17 Nov 2006 02:20:03 +0100 |
wenzelm |
more robust syntax for definition/abbreviation/notation;
|
file |
diff |
annotate
|
| Thu, 16 Nov 2006 20:19:50 +0100 |
huffman |
add lemmas LIM_zero_iff, LIM_norm_zero_iff
|
file |
diff |
annotate
|
| Fri, 10 Nov 2006 00:46:00 +0100 |
huffman |
added bounded_linear and bounded_bilinear locales
|
file |
diff |
annotate
|
| Thu, 09 Nov 2006 00:19:16 +0100 |
huffman |
added LIM_norm and related lemmas
|
file |
diff |
annotate
|
| Wed, 08 Nov 2006 02:13:02 +0100 |
huffman |
LIM_compose -> isCont_LIM_compose;
|
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
|
| Wed, 01 Nov 2006 17:57:02 +0100 |
huffman |
move DERIV_sumr from Series.thy to Lim.thy
|
file |
diff |
annotate
|
| Wed, 01 Nov 2006 17:14:16 +0100 |
huffman |
generalize type of lemma isCont_Id
|
file |
diff |
annotate
|
| Sun, 01 Oct 2006 03:07:12 +0200 |
huffman |
generalize more DERIV proofs
|
file |
diff |
annotate
|
| Sat, 30 Sep 2006 20:54:34 +0200 |
huffman |
generalize proofs of DERIV_isCont and DERIV_mult
|
file |
diff |
annotate
|
| Sat, 30 Sep 2006 19:41:06 +0200 |
huffman |
generalized some DERIV proofs
|
file |
diff |
annotate
|
| Sat, 30 Sep 2006 18:04:28 +0200 |
huffman |
add scaleR lemmas
|
file |
diff |
annotate
|
| Sat, 30 Sep 2006 17:36:55 +0200 |
huffman |
generalize type of DERIV
|
file |
diff |
annotate
|
| Thu, 28 Sep 2006 06:21:06 +0200 |
huffman |
more reorganizing sections
|
file |
diff |
annotate
|
| Thu, 28 Sep 2006 04:03:43 +0200 |
huffman |
reorganize sections
|
file |
diff |
annotate
|
| Thu, 28 Sep 2006 02:50:07 +0200 |
huffman |
add intro/dest rules for NSLIM; rewrite equivalence proofs using transfer
|
file |
diff |
annotate
|
| Thu, 28 Sep 2006 01:26:28 +0200 |
huffman |
generalize type of is(NS)UCont
|
file |
diff |
annotate
|
| Sun, 24 Sep 2006 06:54:39 +0200 |
huffman |
generalize types of lim and nslim
|
file |
diff |
annotate
|
| Thu, 21 Sep 2006 03:17:51 +0200 |
huffman |
removed division_by_zero class requirements from several lemmas
|
file |
diff |
annotate
|
| Wed, 20 Sep 2006 07:44:34 +0200 |
huffman |
change section to subsection
|
file |
diff |
annotate
|
| Mon, 18 Sep 2006 07:48:07 +0200 |
huffman |
replace (x + - y) with (x - y)
|
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
|
| Wed, 30 Aug 2006 03:19:08 +0200 |
webertj |
lin_arith_prover: splitting reverted because of performance loss
|
file |
diff |
annotate
|
| Wed, 23 Aug 2006 22:44:32 +0200 |
huffman |
speed up some proofs
|
file |
diff |
annotate
|
| Sat, 29 Jul 2006 13:15:12 +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
|
| Sun, 12 Feb 2006 12:29:01 +0100 |
kleing |
* include generalised MVT in HyperReal (contributed by Benjamin Porter)
|
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, 27 Jul 2005 11:28:18 +0200 |
paulson |
removed the dependence on abs_mult
|
file |
diff |
annotate
|
| Mon, 21 Feb 2005 15:04:10 +0100 |
nipkow |
comprehensive cleanup, replacing sumr by setsum
|
file |
diff |
annotate
|
| Thu, 02 Dec 2004 11:42:01 +0100 |
nipkow |
Added "ALL x > y" and relatives.
|
file |
diff |
annotate
|
| Tue, 19 Oct 2004 18:18:45 +0200 |
paulson |
converted some induct_tac to induct
|
file |
diff |
annotate
|
| Thu, 07 Oct 2004 15:42:30 +0200 |
paulson |
simplification tweaks for better arithmetic reasoning
|
file |
diff |
annotate
|
| Mon, 04 Oct 2004 15:28:03 +0200 |
paulson |
revised simprules for division
|
file |
diff |
annotate
|
| Fri, 10 Sep 2004 00:19:15 +0200 |
nipkow |
new forward deduction capability for simplifier
|
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
|
| Wed, 28 Jul 2004 16:25:28 +0200 |
paulson |
fixed precedences
|
file |
diff |
annotate
|