| Wed, 03 Dec 2008 15:58:44 +0100 |
haftmann |
made repository layout more coherent with logical distribution structure; stripped some $Id$s
|
file |
diff |
annotate
|
| Mon, 01 Dec 2008 15:36:48 -0800 |
huffman |
clean up imports related to ContNotDenum
|
file |
diff |
annotate
|
| 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
|