author | haftmann |
Wed, 02 Jun 2010 22:45:50 +0200 | |
changeset 37300 | 812ff0bbd677 |
parent 37298 | 1f3ca94ccb84 |
parent 37299 | 6315d1bd8388 |
child 37301 | 12790d670662 |
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