src/HOL/HOLCF/Pcpo.thy
changeset 61169 4de9ff3ea29a
parent 58880 0baae4311a9f
child 61998 b66d2ca1f907
     1.1 --- a/src/HOL/HOLCF/Pcpo.thy	Sun Sep 13 22:25:21 2015 +0200
     1.2 +++ b/src/HOL/HOLCF/Pcpo.thy	Sun Sep 13 22:56:52 2015 +0200
     1.3 @@ -198,7 +198,7 @@
     1.4  begin
     1.5  
     1.6  subclass cpo
     1.7 -apply default
     1.8 +apply standard
     1.9  apply (frule chfin)
    1.10  apply (blast intro: lub_finch1)
    1.11  done
    1.12 @@ -213,7 +213,7 @@
    1.13  begin
    1.14  
    1.15  subclass chfin
    1.16 -apply default
    1.17 +apply standard
    1.18  apply (unfold max_in_chain_def)
    1.19  apply (case_tac "\<forall>i. Y i = \<bottom>")
    1.20  apply simp