| changeset 37299 | 6315d1bd8388 |
| parent 37107 | 1535aa1c943a |
| child 37700 | bd90378b8171 |
| 37295:5c0499f4f4c8 | 37299:6315d1bd8388 |
|---|---|
285 lemma [code]: |
285 lemma [code]: |
286 "mapping_size f g m = 0" |
286 "mapping_size f g m = 0" |
287 by (cases m) simp |
287 by (cases m) simp |
288 |
288 |
289 |
289 |
290 hide_const (open) empty is_empty lookup update delete ordered_keys keys size replace tabulate bulkload |
290 hide_const (open) empty is_empty lookup update delete ordered_keys keys size |
291 replace default map_entry map_default tabulate bulkload |
|
291 |
292 |
292 end |
293 end |