# HG changeset patch
# User huffman
# Date 1120758000 -7200
# Node ID 5608017ee28b5a9984d441da6665a77918b82ad1
# Parent  d0b61beefa495c6a382e4ee655adb078b43e37cb
fixes to work with UU_reorient_simproc

diff -r d0b61beefa49 -r 5608017ee28b src/HOLCF/ex/Stream.thy
--- 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)