src/HOL/HOL.thy
changeset 2912 3fac3e8d5d3e
parent 2762 2ade3a141934
child 3066 3c548f92e032
equal deleted inserted replaced
2911:8a680e310f04 2912:3fac3e8d5d3e
    31 
    31 
    32   Trueprop      :: bool => prop                     ("(_)" 5)
    32   Trueprop      :: bool => prop                     ("(_)" 5)
    33   Not           :: bool => bool                     ("~ _" [40] 40)
    33   Not           :: bool => bool                     ("~ _" [40] 40)
    34   True, False   :: bool
    34   True, False   :: bool
    35   If            :: [bool, 'a, 'a] => 'a   ("(if (_)/ then (_)/ else (_))" 10)
    35   If            :: [bool, 'a, 'a] => 'a   ("(if (_)/ then (_)/ else (_))" 10)
    36   Inv           :: ('a => 'b) => ('b => 'a)
       
    37 
    36 
    38   (* Binders *)
    37   (* Binders *)
    39 
    38 
    40   Eps           :: ('a => bool) => 'a
    39   Eps           :: ('a => bool) => 'a
    41   All           :: ('a => bool) => bool             (binder "! " 10)
    40   All           :: ('a => bool) => bool             (binder "! " 10)
   168 
   167 
   169 defs
   168 defs
   170   (* Misc Definitions *)
   169   (* Misc Definitions *)
   171 
   170 
   172   Let_def       "Let s f == f(s)"
   171   Let_def       "Let s f == f(s)"
   173   Inv_def       "Inv(f::'a=>'b)  == (% y. @x. f(x)=y)"
       
   174   o_def         "(f::'b=>'c) o g == (%(x::'a). f(g(x)))"
   172   o_def         "(f::'b=>'c) o g == (%(x::'a). f(g(x)))"
   175   if_def        "If P x y == @z::'a. (P=True --> z=x) & (P=False --> z=y)"
   173   if_def        "If P x y == @z::'a. (P=True --> z=x) & (P=False --> z=y)"
   176 
   174 
   177 end
   175 end
   178 
   176