author | haftmann |
Wed, 02 Jun 2010 22:45:50 +0200 | |
changeset 37300 | 812ff0bbd677 |
parent 37298 | 1f3ca94ccb84 (current diff) |
parent 37299 | 6315d1bd8388 (diff) |
child 37301 | 12790d670662 |
--- a/src/HOL/Library/Mapping.thy Wed Jun 02 21:53:03 2010 +0200 +++ b/src/HOL/Library/Mapping.thy Wed Jun 02 22:45:50 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