| changeset 60679 | ade12ef2773c |
| parent 60500 | 903bb1495239 |
| child 61068 | 6cb92c2a5ece |
| 60678:17ba2df56dee | 60679:ade12ef2773c |
|---|---|
181 begin |
181 begin |
182 |
182 |
183 definition |
183 definition |
184 "HOL.equal m1 m2 \<longleftrightarrow> (\<forall>k. lookup m1 k = lookup m2 k)" |
184 "HOL.equal m1 m2 \<longleftrightarrow> (\<forall>k. lookup m1 k = lookup m2 k)" |
185 |
185 |
186 instance proof |
186 instance |
187 qed (unfold equal_mapping_def, transfer, auto) |
187 by standard (unfold equal_mapping_def, transfer, auto) |
188 |
188 |
189 end |
189 end |
190 |
190 |
191 context |
191 context |
192 begin |
192 begin |