--- a/src/HOL/Orderings.thy Sat Apr 23 19:49:08 2005 +0200
+++ b/src/HOL/Orderings.thy Sat Apr 23 19:49:16 2005 +0200
@@ -39,7 +39,7 @@
text{* Syntactic sugar: *}
-consts
+syntax
"_gt" :: "'a::ord => 'a => bool" (infixl ">" 50)
"_ge" :: "'a::ord => 'a => bool" (infixl ">=" 50)
translations