| Wed, 09 May 2007 18:25:21 +0200 |
huffman |
add lemma of_hypreal_hyperpow
|
file |
diff |
annotate
|
| Tue, 08 May 2007 23:52:15 +0200 |
huffman |
add lemma Standard_hyperpow
|
file |
diff |
annotate
|
| Tue, 08 May 2007 19:15:35 +0200 |
huffman |
add of_hypreal constant with lemmas
|
file |
diff |
annotate
|
| Sat, 16 Dec 2006 20:23:45 +0100 |
huffman |
moved several theorems; rearranged theory dependencies
|
file |
diff |
annotate
|
| Thu, 14 Dec 2006 22:18:08 +0100 |
huffman |
remove commented section
|
file |
diff |
annotate
|
| Thu, 14 Dec 2006 22:09:26 +0100 |
huffman |
remove ultra tactic and redundant FreeUltrafilterNat lemmas
|
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:46:40 +0100 |
huffman |
consistent naming for FreeUltrafilterNat lemmas; cleaned up
|
file |
diff |
annotate
|
| Wed, 29 Nov 2006 15:44:51 +0100 |
wenzelm |
simplified method setup;
|
file |
diff |
annotate
|
| Fri, 17 Nov 2006 02:20:03 +0100 |
wenzelm |
more robust syntax for definition/abbreviation/notation;
|
file |
diff |
annotate
|
| Tue, 07 Nov 2006 11:47:57 +0100 |
wenzelm |
renamed 'const_syntax' to 'notation';
|
file |
diff |
annotate
|
| Thu, 28 Sep 2006 21:01:13 +0200 |
huffman |
rearranged axioms and simp rules for scaleR
|
file |
diff |
annotate
|
| Thu, 28 Sep 2006 01:32:30 +0200 |
huffman |
add lemma hypreal_epsilon_gt_zero
|
file |
diff |
annotate
|
| Wed, 27 Sep 2006 05:58:42 +0200 |
huffman |
add lemmas of_real_eq_star_of, Reals_eq_Standard
|
file |
diff |
annotate
|
| Wed, 27 Sep 2006 04:19:21 +0200 |
huffman |
add lemmas about Standard, real_of, scaleR
|
file |
diff |
annotate
|
| Tue, 19 Sep 2006 06:22:26 +0200 |
huffman |
added classes real_div_algebra and real_field; added lemmas
|
file |
diff |
annotate
|
| Sat, 16 Sep 2006 19:12:54 +0200 |
huffman |
add instances for real_vector and real_algebra
|
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
|
| Fri, 28 Jul 2006 18:11:22 +0200 |
webertj |
title fixed
|
file |
diff |
annotate
|
| Tue, 20 Jun 2006 15:53:44 +0200 |
ballarin |
Restructured locales with predicates: import is now an interpretation.
|
file |
diff |
annotate
|
| Fri, 02 Jun 2006 23:22:29 +0200 |
wenzelm |
misc cleanup;
|
file |
diff |
annotate
|
| Sun, 09 Apr 2006 18:51:13 +0200 |
wenzelm |
tuned syntax/abbreviations;
|
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 02:13:24 +0200 |
huffman |
added theorem hypreal_inverse2
|
file |
diff |
annotate
|
| Tue, 06 Sep 2005 23:16:48 +0200 |
huffman |
replace type hypreal with real star
|
file |
diff |
annotate
|
| Tue, 06 Sep 2005 19:22:31 +0200 |
huffman |
reimplement Filter.thy with locales
|
file |
diff |
annotate
|
| Fri, 17 Jun 2005 16:12:49 +0200 |
haftmann |
migrated theory headers to new format
|
file |
diff |
annotate
|
| Mon, 21 Feb 2005 15:04:10 +0100 |
nipkow |
comprehensive cleanup, replacing sumr by setsum
|
file |
diff |
annotate
|
| Wed, 15 Dec 2004 17:32:40 +0100 |
paulson |
removal of archaic Abs/Rep proofs
|
file |
diff |
annotate
|