src/HOL/Orderings.thy
changeset 25207 d58c14280367
parent 25193 e2e1a4b00de3
child 25377 dcde128c84a2
     1.1 --- a/src/HOL/Orderings.thy	Fri Oct 26 21:22:17 2007 +0200
     1.2 +++ b/src/HOL/Orderings.thy	Fri Oct 26 21:22:18 2007 +0200
     1.3 @@ -20,11 +20,6 @@
     1.4    assumes antisym: "x \<le> y \<Longrightarrow> y \<le> x \<Longrightarrow> x = y"
     1.5  begin
     1.6  
     1.7 -notation (input)
     1.8 -  less_eq (infix "\<sqsubseteq>" 50)
     1.9 -and
    1.10 -  less    (infix "\<sqsubset>" 50)
    1.11 -
    1.12  text {* Reflexivity. *}
    1.13  
    1.14  lemma eq_refl: "x = y \<Longrightarrow> x \<le> y"
    1.15 @@ -124,7 +119,7 @@
    1.16  subsection {* Linear (total) orders *}
    1.17  
    1.18  class linorder = order +
    1.19 -  assumes linear: "x \<sqsubseteq> y \<or> y \<sqsubseteq> x"
    1.20 +  assumes linear: "x \<le> y \<or> y \<le> x"
    1.21  begin
    1.22  
    1.23  lemma less_linear: "x < y \<or> x = y \<or> y < x"