merged
authorhaftmann
Wed, 02 Jun 2010 22:45:50 +0200
changeset 37300812ff0bbd677
parent 37298 1f3ca94ccb84
parent 37299 6315d1bd8388
child 37301 12790d670662
merged
     1.1 --- a/src/HOL/Library/Mapping.thy	Wed Jun 02 21:53:03 2010 +0200
     1.2 +++ b/src/HOL/Library/Mapping.thy	Wed Jun 02 22:45:50 2010 +0200
     1.3 @@ -287,6 +287,7 @@
     1.4    by (cases m) simp
     1.5  
     1.6  
     1.7 -hide_const (open) empty is_empty lookup update delete ordered_keys keys size replace tabulate bulkload
     1.8 +hide_const (open) empty is_empty lookup update delete ordered_keys keys size
     1.9 +  replace default map_entry map_default tabulate bulkload
    1.10  
    1.11  end
    1.12 \ No newline at end of file