src/HOL/HOLCF/Sfun.thy
changeset 61998 b66d2ca1f907
parent 58880 0baae4311a9f
child 62175 8ffc4d0e652d
--- a/src/HOL/HOLCF/Sfun.thy	Wed Dec 30 21:10:19 2015 +0100
+++ b/src/HOL/HOLCF/Sfun.thy	Wed Dec 30 21:23:38 2015 +0100
@@ -8,12 +8,12 @@
 imports Cfun
 begin
 
-pcpodef ('a, 'b) sfun (infixr "->!" 0)
+pcpodef ('a, 'b) sfun (infixr "\<rightarrow>!" 0)
   = "{f :: 'a \<rightarrow> 'b. f\<cdot>\<bottom> = \<bottom>}"
 by simp_all
 
-type_notation (xsymbols)
-  sfun  (infixr "\<rightarrow>!" 0)
+type_notation (ASCII)
+  sfun  (infixr "->!" 0)
 
 text {* TODO: Define nice syntax for abstraction, application. *}