1.1 --- a/src/HOL/Probability/Projective_Limit.thy	Thu Nov 15 15:50:01 2012 +0100
     1.2 +++ b/src/HOL/Probability/Projective_Limit.thy	Thu Nov 15 16:07:52 2012 +0100
     1.3 @@ -620,6 +620,17 @@
     1.4  
     1.5  end
     1.6  
     1.7 +hide_const (open) PiF
     1.8 +hide_const (open) Pi\<^isub>F
     1.9 +hide_const (open) Pi'
    1.10 +hide_const (open) Abs_finmap
    1.11 +hide_const (open) Rep_finmap
    1.12 +hide_const (open) finmap_of
    1.13 +hide_const (open) finmapset
    1.14 +hide_const (open) proj
    1.15 +hide_const (open) domain
    1.16 +hide_const (open) enum_basis_finmap
    1.17 +
    1.18  sublocale polish_projective \<subseteq> P!: prob_space "(PiB I P)"
    1.19  proof
    1.20    show "emeasure (PiB I P) (space (PiB I P)) = 1"