1.1 --- a/NEWS	Wed Jul 13 23:41:13 2011 +0200
     1.2 +++ b/NEWS	Wed Jul 13 23:49:56 2011 +0200
     1.3 @@ -60,7 +60,7 @@
     1.4  
     1.5  *** HOL ***
     1.6  
     1.7 -* classes bot and top require underlying partial order rather than preorder:
     1.8 +* Classes bot and top require underlying partial order rather than preorder:
     1.9  uniqueness of bot and top is guaranteed.  INCOMPATIBILITY.
    1.10  
    1.11  * Archimedian_Field.thy:

     2.1 --- a/src/HOL/Orderings.thy	Wed Jul 13 23:41:13 2011 +0200
     2.2 +++ b/src/HOL/Orderings.thy	Wed Jul 13 23:49:56 2011 +0200
     2.3 @@ -1088,6 +1088,10 @@
     2.4    assumes bot_least [simp]: "bot \<le> x"
     2.5  begin
     2.6  
     2.7 +lemma bot_unique:
     2.8 +  "a \<le> bot \<longleftrightarrow> a = bot"
     2.9 +  by (auto simp add: intro: antisym)
    2.10 +
    2.11  lemma bot_less:
    2.12    "a \<noteq> bot \<longleftrightarrow> bot < a"
    2.13    by (auto simp add: less_le_not_le intro!: antisym)
    2.14 @@ -1099,6 +1103,10 @@
    2.15    assumes top_greatest [simp]: "x \<le> top"
    2.16  begin
    2.17  
    2.18 +lemma top_unique:
    2.19 +  "top \<le> a \<longleftrightarrow> a = top"
    2.20 +  by (auto simp add: intro: antisym)
    2.21 +
    2.22  lemma less_top:
    2.23    "a \<noteq> top \<longleftrightarrow> a < top"
    2.24    by (auto simp add: less_le_not_le intro!: antisym)