src/HOL/Probability/Projective_Limit.thy
2012-11-19 ago tuned: use induction rule sigma_sets_induct_disjoint
2012-11-19 ago tuned FinMap
2012-11-19 ago merge extensional dependent function space from FuncSet with the one in Finite_Product_Measure
2012-11-16 ago renamed prob_space to proj_prob_space as it clashed with Probability_Measure.prob_space
2012-11-16 ago renamed to more appropriate lim_P for projective limit
2012-11-15 ago corrected headers
2012-11-15 ago hide constants of auxiliary type finmap
2012-11-15 ago added projective limit;