changeset 59487 | adaa430fc0f7 |
parent 58881 | b9556a055632 |
child 60500 | 903bb1495239 |
59486:2025a17bb20f | 59487:adaa430fc0f7 |
---|---|
64 qed |
64 qed |
65 |
65 |
66 lemma [code nbe]: |
66 lemma [code nbe]: |
67 "HOL.equal (x :: ('a, 'b) mapping) x \<longleftrightarrow> True" |
67 "HOL.equal (x :: ('a, 'b) mapping) x \<longleftrightarrow> True" |
68 by (fact equal_refl) |
68 by (fact equal_refl) |
69 |
69 |
70 end |
70 end |
71 |