--- a/NEWS Wed Jul 13 23:41:13 2011 +0200
+++ b/NEWS Wed Jul 13 23:49:56 2011 +0200
@@ -60,7 +60,7 @@
*** HOL ***
-* classes bot and top require underlying partial order rather than preorder:
+* Classes bot and top require underlying partial order rather than preorder:
uniqueness of bot and top is guaranteed. INCOMPATIBILITY.
* Archimedian_Field.thy:
--- a/src/HOL/Orderings.thy Wed Jul 13 23:41:13 2011 +0200
+++ b/src/HOL/Orderings.thy Wed Jul 13 23:49:56 2011 +0200
@@ -1088,6 +1088,10 @@
assumes bot_least [simp]: "bot \<le> x"
begin
+lemma bot_unique:
+ "a \<le> bot \<longleftrightarrow> a = bot"
+ by (auto simp add: intro: antisym)
+
lemma bot_less:
"a \<noteq> bot \<longleftrightarrow> bot < a"
by (auto simp add: less_le_not_le intro!: antisym)
@@ -1099,6 +1103,10 @@
assumes top_greatest [simp]: "x \<le> top"
begin
+lemma top_unique:
+ "top \<le> a \<longleftrightarrow> a = top"
+ by (auto simp add: intro: antisym)
+
lemma less_top:
"a \<noteq> top \<longleftrightarrow> a < top"
by (auto simp add: less_le_not_le intro!: antisym)