--- a/src/Doc/Datatypes/Datatypes.thy Wed Nov 06 12:47:50 2013 +0100
+++ b/src/Doc/Datatypes/Datatypes.thy Wed Nov 06 13:00:16 2013 +0100
@@ -1847,12 +1847,14 @@
text {*
\noindent
-A more natural syntax, also supported by Isabelle, is to move corecursive calls
-under constructors:
+Fortunately, it is easy to prove the following lemma, where the corecursive call
+is moved inside the lazy list constructor, thereby eliminating the need for
+@{const lmap}:
*}
- primcorec (*<*)(in late) (*>*)tree\<^sub>i\<^sub>i_of_stream :: "'a stream \<Rightarrow> 'a tree\<^sub>i\<^sub>i" where
+ lemma tree\<^sub>i\<^sub>i_of_stream_alt:
"tree\<^sub>i\<^sub>i_of_stream s = Node\<^sub>i\<^sub>i (shd s) (LCons (tree\<^sub>i\<^sub>i_of_stream (stl s)) LNil)"
+ by (subst tree\<^sub>i\<^sub>i_of_stream.code) simp
text {*
The next example illustrates corecursion through functions, which is a bit