--- a/src/HOLCF/ex/Stream.thy Wed Feb 24 14:20:07 2010 -0800
+++ b/src/HOLCF/ex/Stream.thy Wed Feb 24 16:15:03 2010 -0800
@@ -273,6 +273,7 @@
section "coinduction"
+(* COINDUCTION TEMPORARILY DISABLED
lemma stream_coind_lemma2: "!s1 s2. R s1 s2 --> ft$s1 = ft$s2 & R (rt$s1) (rt$s2) ==> stream_bisim R"
apply (simp add: stream.bisim_def,clarsimp)
apply (case_tac "x=UU",clarsimp)
@@ -286,6 +287,7 @@
apply (erule_tac x="a && y" in allE)
apply (erule_tac x="aa && ya" in allE) back
by auto
+COINDUCTION TEMPORARILY DISABLED *)