src/HOL/HOLCF/Library/Sum_Cpo.thy
changeset 61169 4de9ff3ea29a
parent 58880 0baae4311a9f
child 62175 8ffc4d0e652d
     1.1 --- a/src/HOL/HOLCF/Library/Sum_Cpo.thy	Sun Sep 13 22:25:21 2015 +0200
     1.2 +++ b/src/HOL/HOLCF/Library/Sum_Cpo.thy	Sun Sep 13 22:56:52 2015 +0200
     1.3 @@ -342,7 +342,7 @@
     1.4  
     1.5  lemma deflation_map_sum [domain_deflation]:
     1.6    "\<lbrakk>deflation d1; deflation d2\<rbrakk> \<Longrightarrow> deflation (map_sum' d1 d2)"
     1.7 -apply default
     1.8 +apply standard
     1.9  apply (induct_tac x, simp_all add: deflation.idem)
    1.10  apply (induct_tac x, simp_all add: deflation.below)
    1.11  done