src/LCF/ex/Ex3.thy

 theory Ex3
 imports "../LCF"
 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))"
 
 declare p_strict [simp] p_s [simp]