src/HOL/Orderings.thy

 end
 
 
 subsection {* Partial orderings *}
 
-locale partial_order = preorder + 
+locale order = preorder + 
   assumes antisym: "x \<sqsubseteq> y \<Longrightarrow> y \<sqsubseteq> x \<Longrightarrow> x = y"
 
-context partial_order
+context order
 begin
 
 text {* Asymmetry. *}
 
 lemma less_not_sym: "x \<sqsubset> y \<Longrightarrow> \<not> (y \<sqsubset> x)"

   order_trans: "x <= y ==> y <= z ==> x <= z"
   order_antisym: "x <= y ==> y <= x ==> x = y"
   order_less_le: "(x < y) = (x <= y & x ~= y)"
 
 interpretation order:
-  partial_order ["op \<le> \<Colon> 'a\<Colon>order \<Rightarrow> 'a \<Rightarrow> bool" "op < \<Colon> 'a\<Colon>order \<Rightarrow> 'a \<Rightarrow> bool"]
+  order ["op \<le> \<Colon> 'a\<Colon>order \<Rightarrow> 'a \<Rightarrow> bool" "op < \<Colon> 'a\<Colon>order \<Rightarrow> 'a \<Rightarrow> bool"]
 apply unfold_locales
 apply (rule order_refl)
 apply (erule (1) order_trans)
 apply (rule order_less_le)
 apply (erule (1) order_antisym)
 done
 
 
 subsection {* Linear (total) orders *}
 
-locale linorder = partial_order +
+locale linorder = order +
   assumes linear: "x \<sqsubseteq> y \<or> y \<sqsubseteq> x"
 begin
 
 lemma less_linear: "x \<sqsubset> y \<or> x = y \<or> y \<sqsubset> x"
   unfolding less_le using less_le linear by blast