--- a/src/HOL/Corec_Examples/Tests/Small_Concrete.thy Mon Mar 28 12:05:47 2016 +0200
+++ b/src/HOL/Corec_Examples/Tests/Small_Concrete.thy Mon Mar 28 12:05:47 2016 +0200
@@ -146,11 +146,16 @@
LNil \<Rightarrow> LNil
| LCons x r \<Rightarrow> LCons x (h3 r))"
-corec (friend) fold_map where
+corec fold_map where
"fold_map f a s = (let v = f a (head s) in S v (fold_map f v (tail s)))"
+friend_of_corec fold_map where
+ "fold_map f a s = (let v = f a (head s) in S v (fold_map f v (tail s)))"
+ apply (rule fold_map.code)
+ sorry
-subsection \<open>Coinductie Natural Numbers\<close>
+
+subsection \<open>Coinductive Natural Numbers\<close>
codatatype conat = CoZero | CoSuc conat