src/HOL/Orderings.thy

 
 lemma less_le: "x < y \<longleftrightarrow> x \<le> y \<and> x \<noteq> y"
   by (auto simp add: less_le_not_le intro: antisym)
 
 sublocale order!: ordering less_eq less +  dual_order!: ordering greater_eq greater
-  by default (auto intro: antisym order_trans simp add: less_le)
+  by standard (auto intro: antisym order_trans simp add: less_le)
 
 
 text \<open>Reflexivity.\<close>
 
 lemma le_less: "x \<le> y \<longleftrightarrow> x < y \<or> x = y"

 class order_bot = order + bot +
   assumes bot_least: "\<bottom> \<le> a"
 begin
 
 sublocale bot!: ordering_top greater_eq greater bot
-  by default (fact bot_least)
+  by standard (fact bot_least)
 
 lemma le_bot:
   "a \<le> \<bottom> \<Longrightarrow> a = \<bottom>"
   by (fact bot.extremum_uniqueI)
 

 class order_top = order + top +
   assumes top_greatest: "a \<le> \<top>"
 begin
 
 sublocale top!: ordering_top less_eq less top
-  by default (fact top_greatest)
+  by standard (fact top_greatest)
 
 lemma top_le:
   "\<top> \<le> a \<Longrightarrow> a = \<top>"
   by (fact top.extremum_uniqueI)