src/HOL/List.thy

--- a/src/HOL/List.thy	Wed Jan 13 23:02:28 2016 +0100
+++ b/src/HOL/List.thy	Wed Jan 13 23:07:06 2016 +0100
@@ -5399,7 +5399,7 @@
 apply (case_tac xys, simp_all, blast)
 done
 
-text{* By Mathias Fleury: *}
+text\<open>By Mathias Fleury:\<close>
 lemma lexn_transI:
   assumes "trans r" shows "trans (lexn r n)"
 unfolding trans_def