| Tue, 09 Apr 2013 14:04:41 +0200 |
hoelzl |
remove the within-filter, replace "at" by "at _ within UNIV" (This allows to remove a couple of redundant lemmas)
|
file |
diff |
annotate
|
| Sat, 23 Mar 2013 20:50:39 +0100 |
haftmann |
fundamental revision of big operators on sets
|
file |
diff |
annotate
|
| Fri, 22 Mar 2013 10:41:43 +0100 |
hoelzl |
move first_countable_topology to the HOL image
|
file |
diff |
annotate
|
| Tue, 05 Mar 2013 15:43:14 +0100 |
hoelzl |
use generate_topology for second countable topologies, does not require intersection stable basis
|
file |
diff |
annotate
|
| Wed, 13 Feb 2013 16:35:07 +0100 |
immler |
eliminated union_closed_basis; cleanup Fin_Map
|
file |
diff |
annotate
|
| Wed, 13 Feb 2013 16:35:07 +0100 |
immler |
fine grained instantiations
|
file |
diff |
annotate
|
| Wed, 13 Feb 2013 16:35:07 +0100 |
immler |
use maximum norm for type finmap
|
file |
diff |
annotate
|
| Mon, 14 Jan 2013 17:29:04 +0100 |
hoelzl |
renamed countable_basis_space to second_countable_topology
|
file |
diff |
annotate
|
| Wed, 28 Nov 2012 15:38:12 +0100 |
wenzelm |
tuned syntax, potentially more robust;
|
file |
diff |
annotate
|
| Tue, 27 Nov 2012 13:48:40 +0100 |
immler |
based countable topological basis on Countable_Set
|
file |
diff |
annotate
|
| Tue, 27 Nov 2012 11:29:47 +0100 |
immler |
qualified interpretation of sigma_algebra, to avoid name clashes
|
file |
diff |
annotate
|
| Mon, 19 Nov 2012 16:09:11 +0100 |
hoelzl |
tuned FinMap
|
file |
diff |
annotate
|
| Mon, 19 Nov 2012 12:29:02 +0100 |
hoelzl |
merge extensional dependent function space from FuncSet with the one in Finite_Product_Measure
|
file |
diff |
annotate
|
| Fri, 16 Nov 2012 14:46:23 +0100 |
hoelzl |
renamed measurable_compose -> measurable_finmap_compose, clashed with Sigma_Algebra.measurable_compose
|
file |
diff |
annotate
|
| Fri, 16 Nov 2012 11:22:22 +0100 |
immler |
allow arbitrary enumerations of basis in locale for generation of borel sets
|
file |
diff |
annotate
|
| Thu, 15 Nov 2012 17:36:08 +0100 |
immler |
corrected headers
|
file |
diff |
annotate
|
| Thu, 15 Nov 2012 11:16:58 +0100 |
immler |
added projective limit;
|
file |
diff |
annotate
|