src/HOLCF/Cprod.thy
changeset 25921 0ca392ab7f37
parent 25913 e1b6521c1f94
child 26018 9b5b4bd44f7a
     1.1 --- a/src/HOLCF/Cprod.thy	Wed Jan 16 22:41:49 2008 +0100
     1.2 +++ b/src/HOLCF/Cprod.thy	Thu Jan 17 00:51:20 2008 +0100
     1.3 @@ -306,7 +306,7 @@
     1.4  done
     1.5  
     1.6  instance "*" :: (chfin, chfin) chfin
     1.7 -apply (intro_classes, clarify)
     1.8 +apply intro_classes
     1.9  apply (erule compact_imp_max_in_chain)
    1.10  apply (rule_tac p="\<Squnion>i. Y i" in cprodE, simp)
    1.11  done