src/HOL/Orderings.thy
changeset 22068 00bed5ac9884
parent 21818 4d2ad5445c81
child 22206 8cc04341de38
     1.1 --- a/src/HOL/Orderings.thy	Tue Jan 16 08:06:55 2007 +0100
     1.2 +++ b/src/HOL/Orderings.thy	Tue Jan 16 08:06:57 2007 +0100
     1.3 @@ -122,10 +122,10 @@
     1.4  
     1.5  subsection {* Partial orderings *}
     1.6  
     1.7 -locale partial_order = preorder + 
     1.8 +locale order = preorder + 
     1.9    assumes antisym: "x \<sqsubseteq> y \<Longrightarrow> y \<sqsubseteq> x \<Longrightarrow> x = y"
    1.10  
    1.11 -context partial_order
    1.12 +context order
    1.13  begin
    1.14  
    1.15  text {* Asymmetry. *}
    1.16 @@ -181,7 +181,7 @@
    1.17    order_less_le: "(x < y) = (x <= y & x ~= y)"
    1.18  
    1.19  interpretation order:
    1.20 -  partial_order ["op \<le> \<Colon> 'a\<Colon>order \<Rightarrow> 'a \<Rightarrow> bool" "op < \<Colon> 'a\<Colon>order \<Rightarrow> 'a \<Rightarrow> bool"]
    1.21 +  order ["op \<le> \<Colon> 'a\<Colon>order \<Rightarrow> 'a \<Rightarrow> bool" "op < \<Colon> 'a\<Colon>order \<Rightarrow> 'a \<Rightarrow> bool"]
    1.22  apply unfold_locales
    1.23  apply (rule order_refl)
    1.24  apply (erule (1) order_trans)
    1.25 @@ -192,7 +192,7 @@
    1.26  
    1.27  subsection {* Linear (total) orders *}
    1.28  
    1.29 -locale linorder = partial_order +
    1.30 +locale linorder = order +
    1.31    assumes linear: "x \<sqsubseteq> y \<or> y \<sqsubseteq> x"
    1.32  begin
    1.33