src/HOL/Complete_Partial_Order.thy
changeset 61169 4de9ff3ea29a
parent 60758 d8d85a8172b5
child 61689 e4d7972402ed
     1.1 --- a/src/HOL/Complete_Partial_Order.thy	Sun Sep 13 22:25:21 2015 +0200
     1.2 +++ b/src/HOL/Complete_Partial_Order.thy	Sun Sep 13 22:56:52 2015 +0200
     1.3 @@ -293,7 +293,7 @@
     1.4  end
     1.5  
     1.6  instance complete_lattice \<subseteq> ccpo
     1.7 -  by default (fast intro: Sup_upper Sup_least)+
     1.8 +  by standard (fast intro: Sup_upper Sup_least)+
     1.9  
    1.10  lemma lfp_eq_fixp:
    1.11    assumes f: "mono f" shows "lfp f = fixp f"