--- a/src/HOL/Library/AList.thy Tue Jan 10 15:43:16 2012 +0100
+++ b/src/HOL/Library/AList.thy Tue Jan 10 17:14:25 2012 +0100
@@ -173,6 +173,7 @@
hide_const valterm_empty valterm_update random_aux_alist
+hide_fact (open) lookup_def empty_def update_def delete_def map_entry_def filter_def map_default_def
hide_const (open) impl_of lookup empty update delete map_entry filter map_default
end
\ No newline at end of file
--- a/src/HOL/Library/AList_Impl.thy Tue Jan 10 15:43:16 2012 +0100
+++ b/src/HOL/Library/AList_Impl.thy Tue Jan 10 17:14:25 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
--- a/src/HOL/Library/AList_Mapping.thy Tue Jan 10 15:43:16 2012 +0100
+++ b/src/HOL/Library/AList_Mapping.thy Tue Jan 10 17:14:25 2012 +0100
@@ -30,11 +30,11 @@
by (cases xs) (simp_all add: is_empty_def null_def)
lemma update_Mapping [code]:
- "Mapping.update k v (Mapping xs) = Mapping (update k v xs)"
+ "Mapping.update k v (Mapping xs) = Mapping (AList_Impl.update k v xs)"
by (rule mapping_eqI) (simp add: update_conv')
lemma delete_Mapping [code]:
- "Mapping.delete k (Mapping xs) = Mapping (delete k xs)"
+ "Mapping.delete k (Mapping xs) = Mapping (AList_Impl.delete k xs)"
by (rule mapping_eqI) (simp add: delete_conv')
lemma ordered_keys_Mapping [code]: