--- a/src/HOLCF/ex/Stream.thy Thu Jul 07 19:18:26 2005 +0200
+++ b/src/HOLCF/ex/Stream.thy Thu Jul 07 19:40:00 2005 +0200
@@ -174,7 +174,7 @@
lemma stream_take_lemma3 [rule_format]:
"ALL x xs. x~=UU --> stream_take n$(x && xs) = x && xs --> stream_take n$xs=xs"
apply (induct_tac n,clarsimp)
-apply (drule sym, erule scons_not_empty, simp)
+(*apply (drule sym, erule scons_not_empty, simp)*)
apply (clarify, rule stream_take_more)
apply (erule_tac x="x" in allE)
by (erule_tac x="xs" in allE,simp)
@@ -356,8 +356,8 @@
apply (simp add: slen_def, auto)
apply (simp add: stream.finite_def, auto)
apply (rule Least_Suc2,auto)
-apply (drule sym)
-apply (drule sym scons_eq_UU [THEN iffD1],simp)
+(*apply (drule sym)*)
+(*apply (drule sym scons_eq_UU [THEN iffD1],simp)*)
apply (erule stream_finite_lemma2, simp)
apply (simp add: slen_def, auto)
by (drule stream_finite_lemma1,auto)
@@ -384,7 +384,7 @@
lemma slen_scons_eq_rev: "(#x < Fin (Suc (Suc n))) = (!a y. x ~= a && y | a = \<bottom> | #y < Fin (Suc n))"
apply (rule stream.casedist [of x], auto)
-apply (drule sym, drule scons_eq_UU [THEN iffD1],auto)
+apply ((*drule sym,*) drule scons_eq_UU [THEN iffD1],auto)
apply (simp add: inat_defs split:inat_splits)
apply (subgoal_tac "s=y & aa=a",simp);
apply (simp add: inat_defs split:inat_splits)
@@ -784,8 +784,8 @@
apply (simp add: i_rt_Suc_forw)
apply (rule_tac x="a && x" in exI,auto)
apply (case_tac "xa=UU",auto)
- apply (drule_tac s="stream_take nat$x" in scons_neq_UU)
- apply (simp add: i_rt_Suc_forw)
+(*apply (drule_tac s="stream_take nat$x" in scons_neq_UU)
+ apply (simp add: i_rt_Suc_forw)*)
apply (drule stream_exhaust_eq [THEN iffD1],auto)
apply (drule streams_prefix_lemma1,simp+)
by (simp add: sconc_def)