src/HOL/Library/Lattice_Constructions.thy
changeset 60679 ade12ef2773c
parent 60509 0928cf63920f
child 62390 842917225d56
     1.1 --- a/src/HOL/Library/Lattice_Constructions.thy	Mon Jul 06 22:06:02 2015 +0200
     1.2 +++ b/src/HOL/Library/Lattice_Constructions.thy	Mon Jul 06 22:57:34 2015 +0200
     1.3 @@ -51,16 +51,16 @@
     1.4    by (simp add: less_bot_def)
     1.5  
     1.6  instance
     1.7 -  by default
     1.8 +  by standard
     1.9      (auto simp add: less_eq_bot_def less_bot_def less_le_not_le elim: order_trans split: bot.splits)
    1.10  
    1.11  end
    1.12  
    1.13  instance bot :: (order) order
    1.14 -  by default (auto simp add: less_eq_bot_def less_bot_def split: bot.splits)
    1.15 +  by standard (auto simp add: less_eq_bot_def less_bot_def split: bot.splits)
    1.16  
    1.17  instance bot :: (linorder) linorder
    1.18 -  by default (auto simp add: less_eq_bot_def less_bot_def split: bot.splits)
    1.19 +  by standard (auto simp add: less_eq_bot_def less_bot_def split: bot.splits)
    1.20  
    1.21  instantiation bot :: (order) bot
    1.22  begin
    1.23 @@ -88,7 +88,7 @@
    1.24          | Value v' \<Rightarrow> Value (inf v v')))"
    1.25  
    1.26  instance
    1.27 -  by default (auto simp add: inf_bot_def less_eq_bot_def split: bot.splits)
    1.28 +  by standard (auto simp add: inf_bot_def less_eq_bot_def split: bot.splits)
    1.29  
    1.30  end
    1.31  
    1.32 @@ -106,7 +106,7 @@
    1.33          | Value v' \<Rightarrow> Value (sup v v')))"
    1.34  
    1.35  instance
    1.36 -  by default (auto simp add: sup_bot_def less_eq_bot_def split: bot.splits)
    1.37 +  by standard (auto simp add: sup_bot_def less_eq_bot_def split: bot.splits)
    1.38  
    1.39  end
    1.40  
    1.41 @@ -158,16 +158,16 @@
    1.42    by (simp add: less_top_def)
    1.43  
    1.44  instance
    1.45 -  by default
    1.46 +  by standard
    1.47      (auto simp add: less_eq_top_def less_top_def less_le_not_le elim: order_trans split: top.splits)
    1.48  
    1.49  end
    1.50  
    1.51  instance top :: (order) order
    1.52 -  by default (auto simp add: less_eq_top_def less_top_def split: top.splits)
    1.53 +  by standard (auto simp add: less_eq_top_def less_top_def split: top.splits)
    1.54  
    1.55  instance top :: (linorder) linorder
    1.56 -  by default (auto simp add: less_eq_top_def less_top_def split: top.splits)
    1.57 +  by standard (auto simp add: less_eq_top_def less_top_def split: top.splits)
    1.58  
    1.59  instantiation top :: (order) top
    1.60  begin
    1.61 @@ -195,7 +195,7 @@
    1.62          | Value v' \<Rightarrow> Value (inf v v')))"
    1.63  
    1.64  instance
    1.65 -  by default (auto simp add: inf_top_def less_eq_top_def split: top.splits)
    1.66 +  by standard (auto simp add: inf_top_def less_eq_top_def split: top.splits)
    1.67  
    1.68  end
    1.69  
    1.70 @@ -213,12 +213,12 @@
    1.71          | Value v' \<Rightarrow> Value (sup v v')))"
    1.72  
    1.73  instance
    1.74 -  by default (auto simp add: sup_top_def less_eq_top_def split: top.splits)
    1.75 +  by standard (auto simp add: sup_top_def less_eq_top_def split: top.splits)
    1.76  
    1.77  end
    1.78  
    1.79  instance top :: (lattice) bounded_lattice_top
    1.80 -  by default (simp add: top_top_def)
    1.81 +  by standard (simp add: top_top_def)
    1.82  
    1.83  
    1.84  subsection \<open>Values extended by a top and a bottom element\<close>
    1.85 @@ -267,7 +267,7 @@
    1.86    by (cases z) (auto simp add: less_eq_flat_complete_lattice_def)
    1.87  
    1.88  instance
    1.89 -  by default
    1.90 +  by standard
    1.91      (auto simp add: less_eq_flat_complete_lattice_def less_flat_complete_lattice_def
    1.92        split: flat_complete_lattice.splits)
    1.93  
    1.94 @@ -313,7 +313,7 @@
    1.95      | Top \<Rightarrow> Top)"
    1.96  
    1.97  instance
    1.98 -  by default
    1.99 +  by standard
   1.100      (auto simp add: inf_flat_complete_lattice_def sup_flat_complete_lattice_def
   1.101        less_eq_flat_complete_lattice_def split: flat_complete_lattice.splits)
   1.102