src/HOLCF/Up.thy
changeset 25898 d8f17d8cf9d4
parent 25879 98b93782c3b1
child 25906 2179c6661218
     1.1 --- a/src/HOLCF/Up.thy	Mon Jan 14 03:56:31 2008 +0100
     1.2 +++ b/src/HOLCF/Up.thy	Mon Jan 14 03:58:30 2008 +0100
     1.3 @@ -344,8 +344,7 @@
     1.4  instance u :: (chfin) chfin
     1.5  apply (intro_classes, clarify)
     1.6  apply (erule compact_imp_max_in_chain)
     1.7 -apply (rule_tac p="\<Squnion>i. Y i" in upE)
     1.8 -apply (simp, simp add: compact_chfin)
     1.9 +apply (rule_tac p="\<Squnion>i. Y i" in upE, simp_all)
    1.10  done
    1.11  
    1.12  text {* properties of fup *}