src/HOL/Orderings.thy
changeset 61169 4de9ff3ea29a
parent 61076 bdc1e2f0a86a
child 61378 3e04c9ca001a
--- a/src/HOL/Orderings.thy	Sun Sep 13 22:25:21 2015 +0200
+++ b/src/HOL/Orderings.thy	Sun Sep 13 22:56:52 2015 +0200
@@ -196,7 +196,7 @@
   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>
@@ -1197,7 +1197,7 @@
 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>"
@@ -1225,7 +1225,7 @@
 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>"