# HG changeset patch
# User wenzelm
# Date 1114278556 -7200
# Node ID 916b9df2ce9fa233b32746f6c4e23fb295fe605b
# Parent  ac7ea72c463bfb6f4fe3b9c45115a3f8a8135b35
_gt, _gt: syntax instead of consts;

diff -r ac7ea72c463b -r 916b9df2ce9f src/HOL/Orderings.thy
--- 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