--- a/src/HOL/Orderings.thy Fri Oct 26 21:22:17 2007 +0200
+++ b/src/HOL/Orderings.thy Fri Oct 26 21:22:18 2007 +0200
@@ -20,11 +20,6 @@
assumes antisym: "x \<le> y \<Longrightarrow> y \<le> x \<Longrightarrow> x = y"
begin
-notation (input)
- less_eq (infix "\<sqsubseteq>" 50)
-and
- less (infix "\<sqsubset>" 50)
-
text {* Reflexivity. *}
lemma eq_refl: "x = y \<Longrightarrow> x \<le> y"
@@ -124,7 +119,7 @@
subsection {* Linear (total) orders *}
class linorder = order +
- assumes linear: "x \<sqsubseteq> y \<or> y \<sqsubseteq> x"
+ assumes linear: "x \<le> y \<or> y \<le> x"
begin
lemma less_linear: "x < y \<or> x = y \<or> y < x"