| 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
|
| 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, 24 Jun 2004 17:52:02 +0200 |
paulson |
replaced monomorphic abs definitions by abs_if
|
file |
diff |
annotate
|
| Fri, 19 Mar 2004 10:51:03 +0100 |
paulson |
conversion of Hyperreal/Lim to new-style
|
file |
diff |
annotate
|
| Sun, 15 Feb 2004 10:46:37 +0100 |
paulson |
Polymorphic treatment of binary arithmetic using axclasses
|
file |
diff |
annotate
|
| Fri, 28 Nov 2003 12:09:37 +0100 |
paulson |
conversion of some Real theories to Isar scripts
|
file |
diff |
annotate
|
| Fri, 07 Feb 2003 16:40:23 +0100 |
nipkow |
(*f -> ( *f because of new comments
|
file |
diff |
annotate
|
| Fri, 02 Nov 2001 17:55:24 +0100 |
paulson |
Numerals and simprocs for types real and hypreal. The abstract
|
file |
diff |
annotate
|
| Sat, 06 Oct 2001 00:02:46 +0200 |
wenzelm |
* sane numerals (stage 2): plain "num" syntax (removed "#");
|
file |
diff |
annotate
|
| Fri, 05 Oct 2001 21:52:39 +0200 |
wenzelm |
sane numerals (stage 1): added generic 1, removed 1' and 2 on nat,
|
file |
diff |
annotate
|
| Sat, 30 Dec 2000 22:03:47 +0100 |
paulson |
separation of HOL-Hyperreal from HOL-Real
|
file |
diff |
annotate
|