| changeset 36176 | 3fe7e97ccca8 |
| parent 36110 | 4ab91a42666a |
| child 37026 | 7e8979a155ae |
--- a/src/HOL/Library/Mapping.thy Fri Apr 16 20:56:40 2010 +0200 +++ b/src/HOL/Library/Mapping.thy Fri Apr 16 21:28:09 2010 +0200 @@ -146,6 +146,6 @@ by (cases m) simp -hide (open) const 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 tabulate bulkload end \ No newline at end of file