merged
authorwenzelm
Sat, 30 Nov 2024 23:30:36 +0100
changeset 81520 878bc24681d9
parent 81502 ed766dfdd2f1 (diff)
parent 81519 cdc43c0fdbfc (current diff)
child 81521 1bfad73ab115
merged
--- a/src/Doc/Datatypes/Datatypes.thy	Sat Nov 30 22:33:21 2024 +0100
+++ b/src/Doc/Datatypes/Datatypes.thy	Sat Nov 30 23:30:36 2024 +0100
@@ -2165,7 +2165,7 @@
 \<close>
 
     primcorec every_snd :: "'a stream \<Rightarrow> 'a stream" where
-      "every_snd s = SCons (shd s) (stl (stl s))"
+      "every_snd s = SCons (shd s) (every_snd (stl (stl s)))"
 
 text \<open>
 \noindent
@@ -2506,7 +2506,7 @@
 
     primcorec every_snd :: "'a stream \<Rightarrow> 'a stream" where
       "shd (every_snd s) = shd s"
-    | "stl (every_snd s) = stl (stl s)"
+    | "stl (every_snd s) = every_snd (stl (stl s))"
 
 text \<open>
 \noindent