--- 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 \<longleftrightarrow> True"
by (fact equal_refl)
-
+
end
+