# HG changeset patch
# User huffman
# Date 1200279510 -3600
# Node ID d8f17d8cf9d4a0f47291cd52307c6aff1e5c66f9
# Parent  e9d45709bece3c8f0a134bd3831c2457cbde73cc
compact_chfin is now declared simp

diff -r e9d45709bece -r d8f17d8cf9d4 src/HOLCF/Up.thy
--- a/src/HOLCF/Up.thy	Mon Jan 14 03:56:31 2008 +0100
+++ b/src/HOLCF/Up.thy	Mon Jan 14 03:58:30 2008 +0100
@@ -344,8 +344,7 @@
 instance u :: (chfin) chfin
 apply (intro_classes, clarify)
 apply (erule compact_imp_max_in_chain)
-apply (rule_tac p="\<Squnion>i. Y i" in upE)
-apply (simp, simp add: compact_chfin)
+apply (rule_tac p="\<Squnion>i. Y i" in upE, simp_all)
 done
 
 text {* properties of fup *}