new: > and >=
authornipkow
Fri Nov 10 16:26:44 2000 +0100 (2000-11-10)
changeset 104279d2de9b6e7f4
parent 10426 469f19c4bf97
child 10428 8f15fbce549f
new: > and >=
src/HOL/Ord.thy
     1.1 --- a/src/HOL/Ord.thy	Fri Nov 10 15:05:09 2000 +0100
     1.2 +++ b/src/HOL/Ord.thy	Fri Nov 10 16:26:44 2000 +0100
     1.3 @@ -59,18 +59,23 @@
     1.4    "_leEx"    :: [idt, 'a, bool] => bool   ("(3EX _<=_./ _)" [0, 0, 10] 10)
     1.5  
     1.6  syntax (symbols)
     1.7 +  "op >="    :: ['a, 'a] => bool          ("(_/ \\<ge> _)"  [50, 51] 50)
     1.8    "_lessAll" :: [idt, 'a, bool] => bool   ("(3\\<forall>_<_./ _)"  [0, 0, 10] 10)
     1.9    "_lessEx"  :: [idt, 'a, bool] => bool   ("(3\\<exists>_<_./ _)"  [0, 0, 10] 10)
    1.10    "_leAll"   :: [idt, 'a, bool] => bool   ("(3\\<forall>_\\<le>_./ _)" [0, 0, 10] 10)
    1.11    "_leEx"    :: [idt, 'a, bool] => bool   ("(3\\<exists>_\\<le>_./ _)" [0, 0, 10] 10)
    1.12  
    1.13  syntax (HOL)
    1.14 +  "op >"     :: ['a, 'a] => bool          ("(_/ > _)"   [50, 51] 50)
    1.15 +  "op >="    :: ['a, 'a] => bool          ("(_/ >= _)"  [50, 51] 50)
    1.16    "_lessAll" :: [idt, 'a, bool] => bool   ("(3! _<_./ _)"  [0, 0, 10] 10)
    1.17    "_lessEx"  :: [idt, 'a, bool] => bool   ("(3? _<_./ _)"  [0, 0, 10] 10)
    1.18    "_leAll"   :: [idt, 'a, bool] => bool   ("(3! _<=_./ _)" [0, 0, 10] 10)
    1.19    "_leEx"    :: [idt, 'a, bool] => bool   ("(3? _<=_./ _)" [0, 0, 10] 10)
    1.20  
    1.21  translations
    1.22 + "x > y"        =>  "y < x"
    1.23 + "x >= y"       =>  "y <= x"
    1.24   "ALL x<y. P"   =>  "ALL x. x < y --> P"
    1.25   "EX x<y. P"    =>  "EX x. x < y  & P"
    1.26   "ALL x<=y. P"  =>  "ALL x. x <= y --> P"