diff -r c09598a97436 -r d8d85a8172b5 src/HOL/Fun_Def_Base.thy
--- a/src/HOL/Fun_Def_Base.thy	Sat Jul 18 21:44:18 2015 +0200
+++ b/src/HOL/Fun_Def_Base.thy	Sat Jul 18 22:58:50 2015 +0200
@@ -2,7 +2,7 @@
     Author:     Alexander Krauss, TU Muenchen
 *)
 
-section {* Function Definition Base *}
+section \<open>Function Definition Base\<close>
 
 theory Fun_Def_Base
 imports Ctr_Sugar Set Wellfounded