haftmann [Fri, 20 May 2011 12:07:17 +0200] rev 43742
point-free characterization of operations on finite sets
haftmann [Fri, 20 May 2011 11:44:34 +0200] rev 43741
merged
haftmann [Fri, 20 May 2011 11:44:16 +0200] rev 43740
names of fold_set locales resemble name of characteristic property more closely
krauss [Fri, 20 May 2011 09:31:36 +0200] rev 43739
clarified vacuous nature of predicate "transfer_morphism" -- equivalent to previous definiton
haftmann [Fri, 20 May 2011 08:16:56 +0200] rev 43738
use point-free characterization for locale fun_left_comm_idem
haftmann [Fri, 20 May 2011 08:16:13 +0200] rev 43737
tuned proof
hoelzl [Tue, 17 May 2011 15:00:39 +0200] rev 43736
Collect intro-rules for sigma-algebras
* * *
sets_Collect shouldn't be intro rules
hoelzl [Tue, 17 May 2011 14:36:54 +0200] rev 43735
the measurable sets with null measure form a ring
hoelzl [Tue, 17 May 2011 12:24:48 +0200] rev 43734
add some lemmas for infinite product measure
hoelzl [Tue, 17 May 2011 12:22:58 +0200] rev 43733
add measurable_Least