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




