src/HOL/HOLCF/Sfun.thy
changeset 62175 8ffc4d0e652d
parent 61998 b66d2ca1f907
child 67312 0d25e02759b7
--- a/src/HOL/HOLCF/Sfun.thy	Wed Jan 13 23:02:28 2016 +0100
+++ b/src/HOL/HOLCF/Sfun.thy	Wed Jan 13 23:07:06 2016 +0100
@@ -2,7 +2,7 @@
     Author:     Brian Huffman
 *)
 
-section {* The Strict Function Type *}
+section \<open>The Strict Function Type\<close>
 
 theory Sfun
 imports Cfun
@@ -15,7 +15,7 @@
 type_notation (ASCII)
   sfun  (infixr "->!" 0)
 
-text {* TODO: Define nice syntax for abstraction, application. *}
+text \<open>TODO: Define nice syntax for abstraction, application.\<close>
 
 definition
   sfun_abs :: "('a \<rightarrow> 'b) \<rightarrow> ('a \<rightarrow>! 'b)"