1.1 --- a/src/HOL/Library/FinFun_Syntax.thy	Wed Jun 17 10:57:11 2015 +0200
     1.2 +++ b/src/HOL/Library/FinFun_Syntax.thy	Wed Jun 17 11:03:05 2015 +0200
     1.3 @@ -1,6 +1,6 @@
     1.4  (* Author: Andreas Lochbihler, KIT *)
     1.5  
     1.6 -section {* Pretty syntax for almost everywhere constant functions *}
     1.7 +section \<open>Pretty syntax for almost everywhere constant functions\<close>
     1.8  
     1.9  theory FinFun_Syntax
    1.10  imports FinFun