| Sun, 28 Aug 2011 09:20:12 -0700 |
huffman |
discontinue many legacy theorems about LIM and LIMSEQ, in favor of tendsto theorems
|
file |
diff |
annotate
|
| Fri, 26 Aug 2011 15:11:26 -0700 |
huffman |
NEWS entry for setsum_norm ~> norm_setsum
|
file |
diff |
annotate
|
| Thu, 25 Aug 2011 19:41:38 -0700 |
huffman |
replace some continuous_on lemmas with more general versions
|
file |
diff |
annotate
|
| Thu, 25 Aug 2011 16:50:55 -0700 |
huffman |
remove legacy theorem Lim_inner
|
file |
diff |
annotate
|
| Thu, 25 Aug 2011 15:35:54 -0700 |
huffman |
remove dot_lsum and dot_rsum in favor of inner_setsum_{left,right}
|
file |
diff |
annotate
|
| Thu, 25 Aug 2011 12:43:55 -0700 |
huffman |
rename subset_{interior,closure} to {interior,closure}_mono;
|
file |
diff |
annotate
|
| Fri, 19 Aug 2011 19:33:31 +0200 |
haftmann |
more concise definition for Inf, Sup on bool
|
file |
diff |
annotate
|
| Thu, 18 Aug 2011 13:36:58 -0700 |
huffman |
remove bounded_(bi)linear locale interpretations, to avoid duplicating so many lemmas
|
file |
diff |
annotate
|
| Thu, 18 Aug 2011 17:42:18 +0200 |
nipkow |
case_names NEWS
|
file |
diff |
annotate
|
| Wed, 10 Aug 2011 13:13:37 -0700 |
huffman |
more uniform naming scheme for finite cartesian product type and related theorems
|
file |
diff |
annotate
|
| Tue, 09 Aug 2011 08:06:15 +0200 |
haftmann |
more uniform naming scheme for Inf/INF and Sup/SUP lemmas
|
file |
diff |
annotate
|
| Tue, 09 Aug 2011 07:44:17 +0200 |
haftmann |
merged
|
file |
diff |
annotate
|
| Mon, 08 Aug 2011 19:21:11 +0200 |
haftmann |
dropped lemmas (Inf|Sup)_(singleton|binary)
|
file |
diff |
annotate
|
| Mon, 08 Aug 2011 19:26:53 -0700 |
huffman |
rename type 'a net to 'a filter, following standard mathematical terminology
|
file |
diff |
annotate
|
| Thu, 04 Aug 2011 07:31:43 +0200 |
haftmann |
NEWS
|
file |
diff |
annotate
|
| Wed, 03 Aug 2011 16:08:02 +0200 |
bulwahn |
NEWS
|
file |
diff |
annotate
|
| Tue, 02 Aug 2011 08:28:34 -0700 |
huffman |
Extended_Nat.thy: renamed iSuc to eSuc, standardized theorem names
|
file |
diff |
annotate
|
| Tue, 02 Aug 2011 07:36:58 -0700 |
huffman |
NEWS: fix typo
|
file |
diff |
annotate
|
| Tue, 02 Aug 2011 12:17:48 +0200 |
krauss |
NEWS
|
file |
diff |
annotate
|
| Mon, 25 Jul 2011 23:27:20 +0200 |
haftmann |
merged
|
file |
diff |
annotate
|
| Sun, 24 Jul 2011 21:27:25 +0200 |
haftmann |
more coherent structure in and across theories
|
file |
diff |
annotate
|
| Mon, 25 Jul 2011 10:42:32 +0200 |
bulwahn |
NEWS
|
file |
diff |
annotate
|
| Wed, 20 Jul 2011 22:14:39 +0200 |
haftmann |
class complete_linorder
|
file |
diff |
annotate
|
| Mon, 18 Jul 2011 21:34:01 +0200 |
haftmann |
avoid misunderstandable names
|
file |
diff |
annotate
|
| Sun, 17 Jul 2011 22:24:08 +0200 |
haftmann |
more on complement
|
file |
diff |
annotate
|
| Sun, 17 Jul 2011 20:57:56 +0200 |
haftmann |
more consistent theorem names
|
file |
diff |
annotate
|
| Sun, 17 Jul 2011 15:15:58 +0200 |
haftmann |
further generalization from sets to complete lattices
|
file |
diff |
annotate
|
| Wed, 13 Jul 2011 23:49:56 +0200 |
haftmann |
uniqueness lemmas for bot and top
|
file |
diff |
annotate
|
| Wed, 13 Jul 2011 23:41:13 +0200 |
haftmann |
adjusted to tightened specification of classes bot and top
|
file |
diff |
annotate
|
| Mon, 11 Jul 2011 17:22:15 +0200 |
wenzelm |
NEWS;
|
file |
diff |
annotate
|