src/HOL/Orderings.thy

   fixes less_eq :: "'a \<Rightarrow> 'a \<Rightarrow> bool"
     and less :: "'a \<Rightarrow> 'a \<Rightarrow> bool"
 begin
 
 notation
-  less_eq  ("op \<^loc><=")
-  less_eq  ("(_/ \<^loc><= _)" [51, 51] 50)
-  less  ("op \<^loc><")
+  less_eq  ("op \<^loc><=") and
+  less_eq  ("(_/ \<^loc><= _)" [51, 51] 50) and
+  less  ("op \<^loc><") and
   less  ("(_/ \<^loc>< _)"  [51, 51] 50)
 
 notation (xsymbols)
-  less_eq  ("op \<^loc>\<le>")
+  less_eq  ("op \<^loc>\<le>") and
   less_eq  ("(_/ \<^loc>\<le> _)"  [51, 51] 50)
 
 notation (HTML output)
-  less_eq  ("op \<^loc>\<le>")
+  less_eq  ("op \<^loc>\<le>") and
   less_eq  ("(_/ \<^loc>\<le> _)"  [51, 51] 50)
 
 abbreviation (input)
-  greater  (infix "\<^loc>>" 50)
+  greater  (infix "\<^loc>>" 50) where
   "x \<^loc>> y \<equiv> y \<^loc>< x"
-  greater_eq  (infix "\<^loc>>=" 50)
+
+abbreviation (input)
+  greater_eq  (infix "\<^loc>>=" 50) where
   "x \<^loc>>= y \<equiv> y \<^loc><= x"
 
 notation (xsymbols)
   greater_eq  (infix "\<^loc>\<ge>" 50)
 
 end
 
 notation
-  less_eq  ("op <=")
-  less_eq  ("(_/ <= _)" [51, 51] 50)
-  less  ("op <")
+  less_eq  ("op <=") and
+  less_eq  ("(_/ <= _)" [51, 51] 50) and
+  less  ("op <") and
   less  ("(_/ < _)"  [51, 51] 50)
   
 notation (xsymbols)
-  less_eq  ("op \<le>")
+  less_eq  ("op \<le>") and
   less_eq  ("(_/ \<le> _)"  [51, 51] 50)
 
 notation (HTML output)
-  less_eq  ("op \<le>")
+  less_eq  ("op \<le>") and
   less_eq  ("(_/ \<le> _)"  [51, 51] 50)
 
 abbreviation (input)
-  greater  (infix ">" 50)
+  greater  (infix ">" 50) where
   "x > y \<equiv> y < x"
-  greater_eq  (infix ">=" 50)
+
+abbreviation (input)
+  greater_eq  (infix ">=" 50) where
   "x >= y \<equiv> y <= x"
   
 notation (xsymbols)
   greater_eq  (infix "\<ge>" 50)
 

   and trans: "x \<sqsubseteq> y \<Longrightarrow> y \<sqsubseteq> z \<Longrightarrow> x \<sqsubseteq> z"
   and less_le: "x \<sqsubset> y \<longleftrightarrow> x \<sqsubseteq> y \<and> x \<noteq> y"
 begin
 
 abbreviation (input)
-  greater_eq (infixl "\<sqsupseteq>" 50)
+  greater_eq  (infixl "\<sqsupseteq>" 50) where
   "x \<sqsupseteq> y \<equiv> y \<sqsubseteq> x"
 
 abbreviation (input)
-  greater (infixl "\<sqsupset>" 50)
+  greater (infixl "\<sqsupset>" 50) where
   "x \<sqsupset> y \<equiv> y \<sqsubset> x"
 
 text {* Reflexivity. *}
 
 lemma eq_refl: "x = y \<Longrightarrow> x \<sqsubseteq> y"

 
 subsection {* Linear (total) orders *}
 
 locale linorder = partial_order +
   assumes linear: "x \<sqsubseteq> y \<or> y \<sqsubseteq> x"
-
-context linorder
 begin
 
 lemma trichotomy: "x \<sqsubset> y \<or> x = y \<or> y \<sqsubset> x"
   unfolding less_le using less_le linear by blast 
 

   unfolding not_le .
 
 (* min/max *)
 
 definition
-  min :: "'a \<Rightarrow> 'a \<Rightarrow> 'a"
+  min :: "'a \<Rightarrow> 'a \<Rightarrow> 'a" where
   "min a b = (if a \<sqsubseteq> b then a else b)"
-  max :: "'a \<Rightarrow> 'a \<Rightarrow> 'a"
+
+definition
+  max :: "'a \<Rightarrow> 'a \<Rightarrow> 'a" where
   "max a b = (if a \<sqsubseteq> b then b else a)"
 
 lemma min_le_iff_disj:
   "min x y \<sqsubseteq> z \<longleftrightarrow> x \<sqsubseteq> z \<or> y \<sqsubseteq> z"
   unfolding min_def using linear by (auto intro: trans)