src/HOL/HOLCF/Fun_Cpo.thy
changeset 61169 4de9ff3ea29a
parent 58880 0baae4311a9f
child 62175 8ffc4d0e652d
     1.1 --- a/src/HOL/HOLCF/Fun_Cpo.thy	Sun Sep 13 22:25:21 2015 +0200
     1.2 +++ b/src/HOL/HOLCF/Fun_Cpo.thy	Sun Sep 13 22:56:52 2015 +0200
     1.3 @@ -93,7 +93,7 @@
     1.4  by (simp add: below_fun_def)
     1.5  
     1.6  instance "fun"  :: (type, pcpo) pcpo
     1.7 -by default (fast intro: minimal_fun)
     1.8 +by standard (fast intro: minimal_fun)
     1.9  
    1.10  lemma inst_fun_pcpo: "\<bottom> = (\<lambda>x. \<bottom>)"
    1.11  by (rule minimal_fun [THEN bottomI, symmetric])