--- a/src/HOLCF/FOCUS/Stream_adm.thy Wed Feb 20 14:52:38 2008 +0100
+++ b/src/HOLCF/FOCUS/Stream_adm.thy Wed Feb 20 18:28:16 2008 +0100
@@ -54,7 +54,7 @@
apply (subst slen_infinite)
apply (erule thin_rl)
apply (drule spec)
-apply (fold ile_def)
+apply (unfold linorder_not_less)
apply (erule ile_iless_trans [THEN Infty_eq [THEN iffD1]])
apply (simp)
done
@@ -142,7 +142,7 @@
apply (erule conjE)
apply (case_tac "#x < Fin i")
apply ( fast)
-apply (fold ile_def)
+apply (unfold linorder_not_less)
apply (drule (1) mp)
apply (erule all_dupE, drule mp, rule refl_less)
apply (erule ssubst)
--- a/src/HOLCF/ex/Stream.thy Wed Feb 20 14:52:38 2008 +0100
+++ b/src/HOLCF/ex/Stream.thy Wed Feb 20 18:28:16 2008 +0100
@@ -433,7 +433,7 @@
by (simp add: inat_defs split:inat_splits)
lemma slen_take_eq_rev: "(#x <= Fin n) = (stream_take n\<cdot>x = x)"
-by (simp add: ile_def slen_take_eq)
+by (simp add: linorder_not_less [symmetric] slen_take_eq)
lemma slen_take_lemma1: "#x = Fin n ==> stream_take n\<cdot>x = x"
by (rule slen_take_eq_rev [THEN iffD1], auto)