src/LCF/ex/Ex3.thy

--- a/src/LCF/ex/Ex3.thy	Tue Nov 11 13:50:56 2014 +0100
+++ b/src/LCF/ex/Ex3.thy	Tue Nov 11 15:55:31 2014 +0100
@@ -5,8 +5,8 @@
 begin
 
 axiomatization
-  s     :: "'a => 'a" and
-  p     :: "'a => 'a => 'a"
+  s     :: "'a \<Rightarrow> 'a" and
+  p     :: "'a \<Rightarrow> 'a \<Rightarrow> 'a"
 where
   p_strict:     "p(UU) = UU" and
   p_s:          "p(s(x),y) = s(p(x,y))"