# HG changeset patch
# User nipkow
# Date 973870004 -3600
# Node ID 9d2de9b6e7f45621905c8023e58c5a84d5d7c3b1
# Parent  469f19c4bf9774220414076a7d72822a8171d876
new: > and >=

diff -r 469f19c4bf97 -r 9d2de9b6e7f4 src/HOL/Ord.thy
--- a/src/HOL/Ord.thy	Fri Nov 10 15:05:09 2000 +0100
+++ b/src/HOL/Ord.thy	Fri Nov 10 16:26:44 2000 +0100
@@ -59,18 +59,23 @@
   "_leEx"    :: [idt, 'a, bool] => bool   ("(3EX _<=_./ _)" [0, 0, 10] 10)
 
 syntax (symbols)
+  "op >="    :: ['a, 'a] => bool          ("(_/ \\<ge> _)"  [50, 51] 50)
   "_lessAll" :: [idt, 'a, bool] => bool   ("(3\\<forall>_<_./ _)"  [0, 0, 10] 10)
   "_lessEx"  :: [idt, 'a, bool] => bool   ("(3\\<exists>_<_./ _)"  [0, 0, 10] 10)
   "_leAll"   :: [idt, 'a, bool] => bool   ("(3\\<forall>_\\<le>_./ _)" [0, 0, 10] 10)
   "_leEx"    :: [idt, 'a, bool] => bool   ("(3\\<exists>_\\<le>_./ _)" [0, 0, 10] 10)
 
 syntax (HOL)
+  "op >"     :: ['a, 'a] => bool          ("(_/ > _)"   [50, 51] 50)
+  "op >="    :: ['a, 'a] => bool          ("(_/ >= _)"  [50, 51] 50)
   "_lessAll" :: [idt, 'a, bool] => bool   ("(3! _<_./ _)"  [0, 0, 10] 10)
   "_lessEx"  :: [idt, 'a, bool] => bool   ("(3? _<_./ _)"  [0, 0, 10] 10)
   "_leAll"   :: [idt, 'a, bool] => bool   ("(3! _<=_./ _)" [0, 0, 10] 10)
   "_leEx"    :: [idt, 'a, bool] => bool   ("(3? _<=_./ _)" [0, 0, 10] 10)
 
 translations
+ "x > y"        =>  "y < x"
+ "x >= y"       =>  "y <= x"
  "ALL x<y. P"   =>  "ALL x. x < y --> P"
  "EX x<y. P"    =>  "EX x. x < y  & P"
  "ALL x<=y. P"  =>  "ALL x. x <= y --> P"