src/HOL/HOL.thy
 changeset 2912 3fac3e8d5d3e parent 2762 2ade3a141934 child 3066 3c548f92e032
equal 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)`
`    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)"`
`   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 `