diff -r 2025a17bb20f -r adaa430fc0f7 src/HOL/Library/AList_Mapping.thy --- a/src/HOL/Library/AList_Mapping.thy Fri Feb 06 19:17:17 2015 +0100 +++ b/src/HOL/Library/AList_Mapping.thy Fri Feb 06 17:57:03 2015 +0100 @@ -66,5 +66,6 @@ lemma [code nbe]: "HOL.equal (x :: ('a, 'b) mapping) x \ True" by (fact equal_refl) - + end +