src/HOL/HOLCF/Map_Functions.thy
changeset 61169 4de9ff3ea29a
parent 58880 0baae4311a9f
child 62175 8ffc4d0e652d
     1.1 --- a/src/HOL/HOLCF/Map_Functions.thy	Sun Sep 13 22:25:21 2015 +0200
     1.2 +++ b/src/HOL/HOLCF/Map_Functions.thy	Sun Sep 13 22:56:52 2015 +0200
     1.3 @@ -195,13 +195,13 @@
     1.4  by (simp add: cfcomp1 u_map_map eta_cfun)
     1.5  
     1.6  lemma ep_pair_u_map: "ep_pair e p \<Longrightarrow> ep_pair (u_map\<cdot>e) (u_map\<cdot>p)"
     1.7 -apply default
     1.8 +apply standard
     1.9  apply (case_tac x, simp, simp add: ep_pair.e_inverse)
    1.10  apply (case_tac y, simp, simp add: ep_pair.e_p_below)
    1.11  done
    1.12  
    1.13  lemma deflation_u_map: "deflation d \<Longrightarrow> deflation (u_map\<cdot>d)"
    1.14 -apply default
    1.15 +apply standard
    1.16  apply (case_tac x, simp, simp add: deflation.idem)
    1.17  apply (case_tac x, simp, simp add: deflation.below)
    1.18  done