src/HOL/Conditionally_Complete_Lattices.thy
changeset 61169 4de9ff3ea29a
parent 60758 d8d85a8172b5
child 61824 dcbe9f756ae0
     1.1 --- a/src/HOL/Conditionally_Complete_Lattices.thy	Sun Sep 13 22:25:21 2015 +0200
     1.2 +++ b/src/HOL/Conditionally_Complete_Lattices.thy	Sun Sep 13 22:56:52 2015 +0200
     1.3 @@ -371,7 +371,7 @@
     1.4  end
     1.5  
     1.6  instance complete_lattice \<subseteq> conditionally_complete_lattice
     1.7 -  by default (auto intro: Sup_upper Sup_least Inf_lower Inf_greatest)
     1.8 +  by standard (auto intro: Sup_upper Sup_least Inf_lower Inf_greatest)
     1.9  
    1.10  lemma cSup_eq:
    1.11    fixes a :: "'a :: {conditionally_complete_lattice, no_bot}"