Mercurial Mercurial > repos > isabelle / comparison
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | file | latest | revisions | annotate | diff | comparison | raw | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
src/HOL/Ord.thy
changeset 10460 a8d9a79ed95e
parent 10427 9d2de9b6e7f4
child 11140 a46eaedbeb2d
equal deleted inserted replaced
10459:df3cd3e76046 10460:a8d9a79ed95e 
    57   "_lessEx"  :: [idt, 'a, bool] => bool   ("(3EX _<_./ _)"  [0, 0, 10] 10)
 
    57   "_lessEx"  :: [idt, 'a, bool] => bool   ("(3EX _<_./ _)"  [0, 0, 10] 10)
 
    58   "_leAll"   :: [idt, 'a, bool] => bool   ("(3ALL _<=_./ _)" [0, 0, 10] 10)
 
    58   "_leAll"   :: [idt, 'a, bool] => bool   ("(3ALL _<=_./ _)" [0, 0, 10] 10)
 
    59   "_leEx"    :: [idt, 'a, bool] => bool   ("(3EX _<=_./ _)" [0, 0, 10] 10)
 
    59   "_leEx"    :: [idt, 'a, bool] => bool   ("(3EX _<=_./ _)" [0, 0, 10] 10)
 
    60 
    60 
    61 syntax (symbols)
 
    61 syntax (symbols)
 
    62   "op >="    :: ['a, 'a] => bool          ("(_/ \\<ge> _)"  [50, 51] 50)
 
       
    63   "_lessAll" :: [idt, 'a, bool] => bool   ("(3\\<forall>_<_./ _)"  [0, 0, 10] 10)
 
    62   "_lessAll" :: [idt, 'a, bool] => bool   ("(3\\<forall>_<_./ _)"  [0, 0, 10] 10)
 
    64   "_lessEx"  :: [idt, 'a, bool] => bool   ("(3\\<exists>_<_./ _)"  [0, 0, 10] 10)
 
    63   "_lessEx"  :: [idt, 'a, bool] => bool   ("(3\\<exists>_<_./ _)"  [0, 0, 10] 10)
 
    65   "_leAll"   :: [idt, 'a, bool] => bool   ("(3\\<forall>_\\<le>_./ _)" [0, 0, 10] 10)
 
    64   "_leAll"   :: [idt, 'a, bool] => bool   ("(3\\<forall>_\\<le>_./ _)" [0, 0, 10] 10)
 
    66   "_leEx"    :: [idt, 'a, bool] => bool   ("(3\\<exists>_\\<le>_./ _)" [0, 0, 10] 10)
 
    65   "_leEx"    :: [idt, 'a, bool] => bool   ("(3\\<exists>_\\<le>_./ _)" [0, 0, 10] 10)
 
    67 
    66 
    68 syntax (HOL)
 
    67 syntax (HOL)
 
    69   "op >"     :: ['a, 'a] => bool          ("(_/ > _)"   [50, 51] 50)
 
       
    70   "op >="    :: ['a, 'a] => bool          ("(_/ >= _)"  [50, 51] 50)
 
       
    71   "_lessAll" :: [idt, 'a, bool] => bool   ("(3! _<_./ _)"  [0, 0, 10] 10)
 
    68   "_lessAll" :: [idt, 'a, bool] => bool   ("(3! _<_./ _)"  [0, 0, 10] 10)
 
    72   "_lessEx"  :: [idt, 'a, bool] => bool   ("(3? _<_./ _)"  [0, 0, 10] 10)
 
    69   "_lessEx"  :: [idt, 'a, bool] => bool   ("(3? _<_./ _)"  [0, 0, 10] 10)
 
    73   "_leAll"   :: [idt, 'a, bool] => bool   ("(3! _<=_./ _)" [0, 0, 10] 10)
 
    70   "_leAll"   :: [idt, 'a, bool] => bool   ("(3! _<=_./ _)" [0, 0, 10] 10)
 
    74   "_leEx"    :: [idt, 'a, bool] => bool   ("(3? _<=_./ _)" [0, 0, 10] 10)
 
    71   "_leEx"    :: [idt, 'a, bool] => bool   ("(3? _<=_./ _)" [0, 0, 10] 10)
 
    75 
    72 
    76 translations
 
    73 translations
 
    77  "x > y"        =>  "y < x"
 
       
    78  "x >= y"       =>  "y <= x"
 
       
    79  "ALL x<y. P"   =>  "ALL x. x < y --> P"
 
    74  "ALL x<y. P"   =>  "ALL x. x < y --> P"
 
    80  "EX x<y. P"    =>  "EX x. x < y  & P"
 
    75  "EX x<y. P"    =>  "EX x. x < y  & P"
 
    81  "ALL x<=y. P"  =>  "ALL x. x <= y --> P"
 
    76  "ALL x<=y. P"  =>  "ALL x. x <= y --> P"
 
    82  "EX x<=y. P"   =>  "EX x. x <= y & P"
 
    77  "EX x<=y. P"   =>  "EX x. x <= y & P"
 
    83 
    78
isabelle