src/HOL/Ord.thy
changeset 6855 36de02d1a257
parent 6515 18e113be12ee
child 7238 36e58620ffc8
equal deleted inserted replaced
6854:60a5ee0ca81d 6855:36de02d1a257
    64   "@leEx"    :: [idt, 'a, bool] => bool   ("(3? _<=_./ _)" [0, 0, 10] 10)
    64   "@leEx"    :: [idt, 'a, bool] => bool   ("(3? _<=_./ _)" [0, 0, 10] 10)
    65 translations
    65 translations
    66  "! x<y.  P"  =>  "! x. x < y  --> P"
    66  "! x<y.  P"  =>  "! x. x < y  --> P"
    67  "! x<=y. P"  =>  "! x. x <= y --> P"
    67  "! x<=y. P"  =>  "! x. x <= y --> P"
    68  "? x<y.  P"  =>  "? x. x < y  & P"
    68  "? x<y.  P"  =>  "? x. x < y  & P"
    69  "? x<=y. P"  =>  "! x. x <= y & P"
    69  "? x<=y. P"  =>  "? x. x <= y & P"
    70 
    70 
    71 end
    71 end