Mercurial Mercurial > repos > isabelle / diff
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | file | latest | revisions | annotate | diff | comparison | raw | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
src/HOLCF/FOCUS/Fstream.thy
changeset 40771 1c6f7d4b110e
parent 40431 682d6c455670 
--- a/src/HOLCF/FOCUS/Fstream.thy	Sat Nov 27 12:55:12 2010 -0800
+++ b/src/HOLCF/FOCUS/Fstream.thy	Sat Nov 27 13:12:10 2010 -0800
@@ -225,7 +225,7 @@
 lemma fstream_lub_lemma1:
     "\<lbrakk>chain Y; (\<Squnion>i. Y i) = a\<leadsto>s\<rbrakk> \<Longrightarrow> \<exists>j t. Y j = a\<leadsto>t"
 apply (case_tac "max_in_chain i Y")
-apply  (drule (1) lub_finch1 [THEN thelubI, THEN sym])
+apply  (drule (1) lub_finch1 [THEN lub_eqI, THEN sym])
 apply  (force)
 apply (unfold max_in_chain_def)
 apply auto
@@ -254,7 +254,7 @@
 apply   (rule chainI)
 apply   (fast)
 apply  (erule chain_shift)
-apply (subst lub_const [THEN thelubI])
+apply (subst lub_const)
 apply (subst lub_range_shift)
 apply  (assumption)
 apply (simp)
isabelle