| changeset 36176 | 3fe7e97ccca8 |
| parent 36110 | 4ab91a42666a |
| child 37026 | 7e8979a155ae |
| 36175:5cec4ca719d1 | 36176:3fe7e97ccca8 |
|---|---|
144 lemma [code]: |
144 lemma [code]: |
145 "mapping_size f g m = 0" |
145 "mapping_size f g m = 0" |
146 by (cases m) simp |
146 by (cases m) simp |
147 |
147 |
148 |
148 |
149 hide (open) const empty is_empty lookup update delete ordered_keys keys size replace tabulate bulkload |
149 hide_const (open) empty is_empty lookup update delete ordered_keys keys size replace tabulate bulkload |
150 |
150 |
151 end |
151 end |