| Mon, 17 Nov 2008 17:00:55 +0100 |
haftmann |
tuned unfold_locales invocation
|
file |
diff |
annotate
|
| Fri, 10 Oct 2008 06:45:53 +0200 |
haftmann |
`code func` now just `code`
|
file |
diff |
annotate
|
| Fri, 25 Jul 2008 12:03:32 +0200 |
haftmann |
dropped locale (open)
|
file |
diff |
annotate
|
| Fri, 11 Jul 2008 09:02:26 +0200 |
haftmann |
explicit dependency
|
file |
diff |
annotate
|
| Wed, 02 Jul 2008 07:11:57 +0200 |
haftmann |
cleaned up some code generator configuration
|
file |
diff |
annotate
|
| Mon, 28 Apr 2008 20:21:11 +0200 |
haftmann |
thms Max_ge, Min_le: dropped superfluous premise
|
file |
diff |
annotate
|
| Mon, 17 Mar 2008 22:34:26 +0100 |
wenzelm |
avoid rebinding of existing facts;
|
file |
diff |
annotate
|
| Sun, 24 Jun 2007 20:55:41 +0200 |
nipkow |
tuned and used field_simps
|
file |
diff |
annotate
|
| Sat, 23 Jun 2007 19:33:22 +0200 |
nipkow |
tuned and renamed group_eq_simps and ring_eq_simps
|
file |
diff |
annotate
|
| Wed, 30 May 2007 02:41:26 +0200 |
huffman |
simplify names of locale interpretations
|
file |
diff |
annotate
|
| Thu, 17 May 2007 21:51:32 +0200 |
huffman |
avoid using redundant lemmas from RealDef.thy
|
file |
diff |
annotate
|
| Mon, 14 May 2007 22:32:51 +0200 |
huffman |
tuned proofs
|
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
|
| Wed, 11 Apr 2007 02:19:06 +0200 |
huffman |
new standard proof of convergent = Cauchy
|
file |
diff |
annotate
|
| Tue, 10 Apr 2007 22:02:43 +0200 |
huffman |
new standard proof of LIMSEQ_realpow_zero
|
file |
diff |
annotate
|
| Mon, 09 Apr 2007 04:51:28 +0200 |
huffman |
new standard proofs of some LIMSEQ lemmas
|
file |
diff |
annotate
|
| Sun, 08 Apr 2007 18:35:19 +0200 |
huffman |
rearranged sections
|
file |
diff |
annotate
|
| Fri, 06 Apr 2007 01:26:30 +0200 |
huffman |
add new standard proofs for limits of sequences
|
file |
diff |
annotate
|
| Thu, 14 Dec 2006 01:19:27 +0100 |
huffman |
remove references to star_n and FreeUltrafilterNat; new proof of NSBseq_Bseq
|
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
|
| Fri, 17 Nov 2006 02:20:03 +0100 |
wenzelm |
more robust syntax for definition/abbreviation/notation;
|
file |
diff |
annotate
|
| Wed, 01 Nov 2006 16:48:58 +0100 |
huffman |
new proof of Bseq_NSbseq using transfer
|
file |
diff |
annotate
|
| Mon, 02 Oct 2006 21:30:05 +0200 |
huffman |
add axclass banach for complete normed vector spaces
|
file |
diff |
annotate
|
| Mon, 02 Oct 2006 19:57:02 +0200 |
huffman |
remove unused Cauchy_Bseq lemmas
|
file |
diff |
annotate
|
| Thu, 28 Sep 2006 00:57:36 +0200 |
huffman |
add intro/dest rules for (NS)LIMSEQ and (NS)Cauchy; rewrite equivalence proofs using transfer
|
file |
diff |
annotate
|
| Wed, 27 Sep 2006 21:44:38 +0200 |
huffman |
reorganized HNatInfinite proofs; simplified and renamed some lemmas
|
file |
diff |
annotate
|
| Wed, 27 Sep 2006 05:39:29 +0200 |
huffman |
move star_of_norm from SEQ.thy to NSA.thy
|
file |
diff |
annotate
|
| Sun, 24 Sep 2006 08:22:21 +0200 |
huffman |
reorganized subsection headings
|
file |
diff |
annotate
|
| Sun, 24 Sep 2006 07:18:16 +0200 |
huffman |
moved SEQ_Infinitesimal from SEQ to HyperNat
|
file |
diff |
annotate
|
| Sun, 24 Sep 2006 06:54:39 +0200 |
huffman |
generalize types of lim and nslim
|
file |
diff |
annotate
|
| Sun, 24 Sep 2006 04:16:28 +0200 |
huffman |
add lemma convergent_Cauchy
|
file |
diff |
annotate
|
| Fri, 22 Sep 2006 23:19:45 +0200 |
huffman |
added lemmas about LIMSEQ and norm; simplified some proofs
|
file |
diff |
annotate
|
| Fri, 22 Sep 2006 16:25:15 +0200 |
huffman |
define constants with THE instead of SOME
|
file |
diff |
annotate
|
| Thu, 21 Sep 2006 03:17:51 +0200 |
huffman |
removed division_by_zero class requirements from several lemmas
|
file |
diff |
annotate
|
| Mon, 18 Sep 2006 07:48:07 +0200 |
huffman |
replace (x + - y) with (x - y)
|
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, 23 Aug 2006 22:12:54 +0200 |
huffman |
generalize proof of SUP_rabs_subseq
|
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
|
| Thu, 05 Jan 2006 22:29:55 +0100 |
wenzelm |
replaced swap by contrapos_np;
|
file |
diff |
annotate
|
| Fri, 16 Sep 2005 20:30:44 +0200 |
huffman |
add header
|
file |
diff |
annotate
|
| Thu, 15 Sep 2005 23:46:22 +0200 |
huffman |
merged Transfer.thy and StarType.thy into StarDef.thy; renamed Ifun2_of to starfun2; cleaned up
|
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
|
| Wed, 07 Sep 2005 00:48:50 +0200 |
huffman |
replace type hypnat with nat star
|
file |
diff |
annotate
|
| Tue, 06 Sep 2005 23:16:48 +0200 |
huffman |
replace type hypreal with real star
|
file |
diff |
annotate
|
| Wed, 13 Jul 2005 19:49:07 +0200 |
avigad |
Additions to the Real (and Hyperreal) libraries:
|
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, 23 Nov 2004 15:32:11 +0100 |
nipkow |
added lemma
|
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
|
| Mon, 11 Oct 2004 07:42:22 +0200 |
nipkow |
Proofs needed to be updated because induction now preserves name of
|
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
|
| Fri, 01 Oct 2004 11:53:31 +0200 |
paulson |
tweaking of arithmetic proofs
|
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
|
| Tue, 03 Aug 2004 13:48:00 +0200 |
paulson |
new simprules Int_subset_iff and Un_subset_iff
|
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:26:27 +0200 |
paulson |
conversion of SEQ.ML to Isar script
|
file |
diff |
annotate
|
| Fri, 07 Feb 2003 16:40:23 +0100 |
nipkow |
(*f -> ( *f because of new comments
|
file |
diff |
annotate
|