
diff -r 54a3db2ed201 -r 903bb1495239 src/HOL/Library/AList_Mapping.thy
--- a/src/HOL/Library/AList_Mapping.thy	Wed Jun 17 10:57:11 2015 +0200
+++ b/src/HOL/Library/AList_Mapping.thy	Wed Jun 17 11:03:05 2015 +0200
@@ -2,7 +2,7 @@
    Author: Florian Haftmann, TU Muenchen
 *)
 
-section {* Implementation of mappings with Association Lists *}
+section \<open>Implementation of mappings with Association Lists\<close>
 
 theory AList_Mapping
 imports AList Mapping




