src/HOL/HOLCF/LowerPD.thy
changeset 61169 4de9ff3ea29a
parent 58880 0baae4311a9f
child 61998 b66d2ca1f907
     1.1 --- a/src/HOL/HOLCF/LowerPD.thy	Sun Sep 13 22:25:21 2015 +0200
     1.2 +++ b/src/HOL/HOLCF/LowerPD.thy	Sun Sep 13 22:56:52 2015 +0200
     1.3 @@ -407,14 +407,14 @@
     1.4  by (simp add: lower_map_def lower_bind_bind)
     1.5  
     1.6  lemma ep_pair_lower_map: "ep_pair e p \<Longrightarrow> ep_pair (lower_map\<cdot>e) (lower_map\<cdot>p)"
     1.7 -apply default
     1.8 +apply standard
     1.9  apply (induct_tac x rule: lower_pd_induct, simp_all add: ep_pair.e_inverse)
    1.10  apply (induct_tac y rule: lower_pd_induct)
    1.11  apply (simp_all add: ep_pair.e_p_below monofun_cfun del: lower_plus_below_iff)
    1.12  done
    1.13  
    1.14  lemma deflation_lower_map: "deflation d \<Longrightarrow> deflation (lower_map\<cdot>d)"
    1.15 -apply default
    1.16 +apply standard
    1.17  apply (induct_tac x rule: lower_pd_induct, simp_all add: deflation.idem)
    1.18  apply (induct_tac x rule: lower_pd_induct)
    1.19  apply (simp_all add: deflation.below monofun_cfun del: lower_plus_below_iff)