# HG changeset patch
# User haftmann
# Date 1275509174 -7200
# Node ID 6315d1bd8388ad3f414f9d9c988355995d528923
# Parent  5c0499f4f4c86aaefb3f38f92efc763215e53dcf
hide default, map_entry, map_default

diff -r 5c0499f4f4c8 -r 6315d1bd8388 src/HOL/Library/Mapping.thy
--- a/src/HOL/Library/Mapping.thy	Wed Jun 02 18:48:30 2010 +0200
+++ b/src/HOL/Library/Mapping.thy	Wed Jun 02 22:06:14 2010 +0200
@@ -287,6 +287,7 @@
   by (cases m) simp
 
 
-hide_const (open) empty is_empty lookup update delete ordered_keys keys size replace tabulate bulkload
+hide_const (open) empty is_empty lookup update delete ordered_keys keys size
+  replace default map_entry map_default tabulate bulkload
 
 end
\ No newline at end of file