changeset 46171 | 19f68d7671f0 |
parent 46133 | d9fe85d3d2cd |
--- a/src/HOL/Library/AList_Impl.thy Tue Jan 10 10:48:39 2012 +0100 +++ b/src/HOL/Library/AList_Impl.thy Tue Jan 10 15:48:10 2012 +0100 @@ -693,6 +693,6 @@ shows "distinct (map fst (map_default k v f xs))" using assms by (induct xs) (auto simp add: dom_map_default) -hide_const (open) map_entry +hide_const (open) update updates delete restrict clearjunk merge compose map_entry end