src/HOL/Orderings.thy
changeset 54868 bab6cade3cc5
parent 54861 00d551179872
child 56020 f92479477c52
     1.1 --- a/src/HOL/Orderings.thy	Thu Dec 26 22:47:49 2013 +0100
     1.2 +++ b/src/HOL/Orderings.thy	Fri Dec 27 14:35:14 2013 +0100
     1.3 @@ -195,13 +195,9 @@
     1.4  lemma less_le: "x < y \<longleftrightarrow> x \<le> y \<and> x \<noteq> y"
     1.5    by (auto simp add: less_le_not_le intro: antisym)
     1.6  
     1.7 -end
     1.8 -
     1.9 -sublocale order < order!: ordering less_eq less +  dual_order!: ordering greater_eq greater
    1.10 +sublocale order!: ordering less_eq less +  dual_order!: ordering greater_eq greater
    1.11    by default (auto intro: antisym order_trans simp add: less_le)
    1.12  
    1.13 -context order
    1.14 -begin
    1.15  
    1.16  text {* Reflexivity. *}
    1.17  
    1.18 @@ -1130,13 +1126,11 @@
    1.19  
    1.20  class order_bot = order + bot +
    1.21    assumes bot_least: "\<bottom> \<le> a"
    1.22 +begin
    1.23  
    1.24 -sublocale order_bot < bot!: ordering_top greater_eq greater bot
    1.25 +sublocale bot!: ordering_top greater_eq greater bot
    1.26    by default (fact bot_least)
    1.27  
    1.28 -context order_bot
    1.29 -begin
    1.30 -
    1.31  lemma le_bot:
    1.32    "a \<le> \<bottom> \<Longrightarrow> a = \<bottom>"
    1.33    by (fact bot.extremum_uniqueI)
    1.34 @@ -1160,13 +1154,11 @@
    1.35  
    1.36  class order_top = order + top +
    1.37    assumes top_greatest: "a \<le> \<top>"
    1.38 +begin
    1.39  
    1.40 -sublocale order_top < top!: ordering_top less_eq less top
    1.41 +sublocale top!: ordering_top less_eq less top
    1.42    by default (fact top_greatest)
    1.43  
    1.44 -context order_top
    1.45 -begin
    1.46 -
    1.47  lemma top_le:
    1.48    "\<top> \<le> a \<Longrightarrow> a = \<top>"
    1.49    by (fact top.extremum_uniqueI)