# HG changeset patch # User haftmann # Date 1191519723 -7200 # Node ID 2bdf31a97362c411a47e4fe0aaf2af1bf8ba26e4 # Parent df8448bc7a8b9b2006d7f9f498aa76d58baa0369 clarified declarations in class ord diff -r df8448bc7a8b -r 2bdf31a97362 src/HOL/HOL.thy --- a/src/HOL/HOL.thy Thu Oct 04 19:41:55 2007 +0200 +++ b/src/HOL/HOL.thy Thu Oct 04 19:42:03 2007 +0200 @@ -263,16 +263,16 @@ less_eq ("(_/ \<^loc>\ _)" [51, 51] 50) abbreviation (input) - greater (infix "\<^loc>>" 50) where - "x \<^loc>> y \ y \<^loc>< x" - -abbreviation (input) greater_eq (infix "\<^loc>>=" 50) where "x \<^loc>>= y \ y \<^loc><= x" notation (input) greater_eq (infix "\<^loc>\" 50) +abbreviation (input) + greater (infix "\<^loc>>" 50) where + "x \<^loc>> y \ y \<^loc>< x" + definition Least :: "('a \ bool) \ 'a" (binder "\<^loc>LEAST " 10) where @@ -294,15 +294,12 @@ less_eq ("op \") and less_eq ("(_/ \ _)" [51, 51] 50) -abbreviation (input) - greater (infix ">" 50) where - "x > y \ y < x" - -abbreviation (input) - greater_eq (infix ">=" 50) where - "x >= y \ y <= x" +notation (input) + greater (infix ">" 50) notation (input) + greater_eq (infix ">=" 50) +and greater_eq (infix "\" 50) syntax