src/HOL/Library/Finite_Lattice.thy
changeset 60679 ade12ef2773c
parent 60500 903bb1495239
child 62343 24106dc44def
     1.1 --- a/src/HOL/Library/Finite_Lattice.thy	Mon Jul 06 22:06:02 2015 +0200
     1.2 +++ b/src/HOL/Library/Finite_Lattice.thy	Mon Jul 06 22:57:34 2015 +0200
     1.3 @@ -32,13 +32,13 @@
     1.4    by (auto simp: bot_def intro: Inf_fin.coboundedI)
     1.5  
     1.6  instance finite_lattice_complete \<subseteq> order_bot
     1.7 -  by default (auto simp: finite_lattice_complete_bot_least)
     1.8 +  by standard (auto simp: finite_lattice_complete_bot_least)
     1.9  
    1.10  lemma finite_lattice_complete_top_greatest: "(top::'a::finite_lattice_complete) \<ge> x"
    1.11    by (auto simp: top_def Sup_fin.coboundedI)
    1.12  
    1.13  instance finite_lattice_complete \<subseteq> order_top
    1.14 -  by default (auto simp: finite_lattice_complete_top_greatest)
    1.15 +  by standard (auto simp: finite_lattice_complete_top_greatest)
    1.16  
    1.17  instance finite_lattice_complete \<subseteq> bounded_lattice ..
    1.18  
    1.19 @@ -124,7 +124,7 @@
    1.20    by (metis Sup_fold_sup finite_code)
    1.21  
    1.22  instance prod :: (finite_lattice_complete, finite_lattice_complete) finite_lattice_complete
    1.23 -  by default (auto simp: finite_bot_prod finite_top_prod finite_Inf_prod finite_Sup_prod)
    1.24 +  by standard (auto simp: finite_bot_prod finite_top_prod finite_Inf_prod finite_Sup_prod)
    1.25  
    1.26  text \<open>Functions with a finite domain and with a finite lattice as codomain
    1.27  already form a finite lattice.\<close>
    1.28 @@ -146,7 +146,7 @@
    1.29    by (metis Sup_fold_sup finite_code)
    1.30  
    1.31  instance "fun" :: (finite, finite_lattice_complete) finite_lattice_complete
    1.32 -  by default (auto simp: finite_bot_fun finite_top_fun finite_Inf_fun finite_Sup_fun)
    1.33 +  by standard (auto simp: finite_bot_fun finite_top_fun finite_Inf_fun finite_Sup_fun)
    1.34  
    1.35  
    1.36  subsection \<open>Finite Distributive Lattices\<close>