| changeset 50124 | 4161c834c2fd |
| parent 50123 | 69b35a75caf3 |
| child 50125 | 4319691be975 |
--- a/src/HOL/Probability/Projective_Limit.thy Mon Nov 19 12:29:02 2012 +0100 +++ b/src/HOL/Probability/Projective_Limit.thy Mon Nov 19 16:09:11 2012 +0100 @@ -626,7 +626,6 @@ hide_const (open) Abs_finmap hide_const (open) Rep_finmap hide_const (open) finmap_of -hide_const (open) finmapset hide_const (open) proj hide_const (open) domain hide_const (open) enum_basis_finmap