compact_chfin is now declared simp
authorhuffman
Mon Jan 14 03:58:30 2008 +0100 (2008-01-14)
changeset 25898d8f17d8cf9d4
parent 25897 e9d45709bece
child 25899 f344ff9e2041
compact_chfin is now declared simp
src/HOLCF/Up.thy
     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 *}