# HG changeset patch
# User wenzelm
# Date 1733005836 -3600
# Node ID 878bc24681d90ae6f92b01a4262d53b846fb6266
# Parent  ed766dfdd2f1b55b0ebfc520fd362bf08ef432b9# Parent  cdc43c0fdbfc299d7333304d9d79c619a9798c7b
merged

diff -r cdc43c0fdbfc -r 878bc24681d9 src/Doc/Datatypes/Datatypes.thy
--- 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