# HG changeset patch
# User huffman
# Date 1213977360 -7200
# Node ID 3628064c4b44c3a8f405843002527924cb2580b9
# Parent  784620cccb80b12806496b3b75840558b1eebf06
replace less_lift with flat_less_iff

diff -r 784620cccb80 -r 3628064c4b44 src/HOLCF/FOCUS/Fstreams.thy
--- a/src/HOLCF/FOCUS/Fstreams.thy	Fri Jun 20 17:43:16 2008 +0200
+++ b/src/HOLCF/FOCUS/Fstreams.thy	Fri Jun 20 17:56:00 2008 +0200
@@ -222,7 +222,7 @@
 apply (case_tac "y=UU", auto)
 apply (drule stream_exhaust_eq [THEN iffD1], auto)
 apply (auto simp add: stream.inverts)
-apply (simp add: less_lift)
+apply (simp add: flat_less_iff)
 apply (case_tac "s=UU", auto)
 apply (drule stream_exhaust_eq [THEN iffD1], auto)
 apply (erule_tac x="ya" in allE)
@@ -230,11 +230,11 @@
 apply (case_tac "y=UU",auto)
 apply (drule stream_exhaust_eq [THEN iffD1], clarsimp)
 apply (auto simp add: stream.inverts)
-apply (simp add: less_lift)
+apply (simp add: flat_less_iff)
 apply (erule_tac x="tt" in allE)
 apply (erule_tac x="yb" in allE, auto)
-apply (simp add: less_lift)
-by (simp add: less_lift)
+apply (simp add: flat_less_iff)
+by (simp add: flat_less_iff)
 
 lemma fstreams_lub_lemma1: "[| chain Y; lub (range Y) = <a> ooo s |] ==> EX j t. Y j = <a> ooo t"
 apply (subgoal_tac "lub(range Y) ~= UU")