src/HOL/Orderings.thy
changeset 61169 4de9ff3ea29a
parent 61076 bdc1e2f0a86a
child 61378 3e04c9ca001a
     1.1 --- a/src/HOL/Orderings.thy	Sun Sep 13 22:25:21 2015 +0200
     1.2 +++ b/src/HOL/Orderings.thy	Sun Sep 13 22:56:52 2015 +0200
     1.3 @@ -196,7 +196,7 @@
     1.4    by (auto simp add: less_le_not_le intro: antisym)
     1.5  
     1.6  sublocale order!: ordering less_eq less +  dual_order!: ordering greater_eq greater
     1.7 -  by default (auto intro: antisym order_trans simp add: less_le)
     1.8 +  by standard (auto intro: antisym order_trans simp add: less_le)
     1.9  
    1.10  
    1.11  text \<open>Reflexivity.\<close>
    1.12 @@ -1197,7 +1197,7 @@
    1.13  begin
    1.14  
    1.15  sublocale bot!: ordering_top greater_eq greater bot
    1.16 -  by default (fact bot_least)
    1.17 +  by standard (fact bot_least)
    1.18  
    1.19  lemma le_bot:
    1.20    "a \<le> \<bottom> \<Longrightarrow> a = \<bottom>"
    1.21 @@ -1225,7 +1225,7 @@
    1.22  begin
    1.23  
    1.24  sublocale top!: ordering_top less_eq less top
    1.25 -  by default (fact top_greatest)
    1.26 +  by standard (fact top_greatest)
    1.27  
    1.28  lemma top_le:
    1.29    "\<top> \<le> a \<Longrightarrow> a = \<top>"