# HG changeset patch
# User nipkow
# Date 974102001 -3600
# Node ID a8d9a79ed95e6668ef1c5eea6179e3a71682029e
# Parent  df3cd3e760466e9d0bc6eb7488fa74effb256c15
Removed > and >= again.

diff -r df3cd3e76046 -r a8d9a79ed95e src/HOL/Ord.thy
--- a/src/HOL/Ord.thy	Sun Nov 12 14:50:26 2000 +0100
+++ b/src/HOL/Ord.thy	Mon Nov 13 08:53:21 2000 +0100
@@ -59,23 +59,18 @@
   "_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"