--- a/src/HOL/Corec_Examples/Tests/Stream_Friends.thy Mon Mar 28 12:05:47 2016 +0200
+++ b/src/HOL/Corec_Examples/Tests/Stream_Friends.thy Mon Mar 28 12:05:47 2016 +0200
@@ -49,7 +49,6 @@
friend_of_corec sthe_default where
"sthe_default s n opt = SCons (shd (case opt of None \<Rightarrow> s | Some t \<Rightarrow> t)) (stl (case opt of None \<Rightarrow> s | Some t \<Rightarrow> t))"
sorry
-*)
corec funky0 :: "nat \<Rightarrow> nat stream" where
"funky0 n = SCons 0 (sthe_default undefined n (map_option funky0 undefined))"
@@ -72,11 +71,9 @@
corec phunky0 :: "nat \<Rightarrow> nat stream" where
"phunky0 n = sthe_default undefined n undefined"
-(* FIXME:
fun lthe_default :: "'a stream \<Rightarrow> 'a stream option \<Rightarrow> 'a stream" where
"lthe_default s None = s"
| "lthe_default _ (Some t) = t"
-*)
friend_of_corec lthe_default where
"lthe_default s opt = SCons (shd (case opt of None \<Rightarrow> s | Some t \<Rightarrow> t)) (stl (case opt of None \<Rightarrow> s | Some t \<Rightarrow> t))"
@@ -95,5 +92,6 @@
corec phunky3 :: "nat \<Rightarrow> nat stream" where
"phunky3 n = sthe_default (SCons 0 (sthe_default (phunky3 (n + 1)) n (map_option phunky3 (Some (n + 3))))) n
(Some (SCons n (sthe_default (phunky3 (n + 1)) n (map_option phunky3 (Some (n + 3))))))"
+*)
end