equal
deleted
inserted
replaced
45 Ex1 :: ('a => bool) => bool (binder "?! " 10) |
45 Ex1 :: ('a => bool) => bool (binder "?! " 10) |
46 Let :: ['a, 'a => 'b] => 'b |
46 Let :: ['a, 'a => 'b] => 'b |
47 |
47 |
48 (* Infixes *) |
48 (* Infixes *) |
49 |
49 |
50 o :: ['b => 'c, 'a => 'b, 'a] => 'c (infixl 55) |
|
51 "=" :: ['a, 'a] => bool (infixl 50) |
50 "=" :: ['a, 'a] => bool (infixl 50) |
52 "&" :: [bool, bool] => bool (infixr 35) |
51 "&" :: [bool, bool] => bool (infixr 35) |
53 "|" :: [bool, bool] => bool (infixr 30) |
52 "|" :: [bool, bool] => bool (infixr 30) |
54 "-->" :: [bool, bool] => bool (infixr 25) |
53 "-->" :: [bool, bool] => bool (infixr 25) |
55 |
54 |
178 True_or_False "(P=True) | (P=False)" |
177 True_or_False "(P=True) | (P=False)" |
179 |
178 |
180 defs |
179 defs |
181 (*misc definitions*) |
180 (*misc definitions*) |
182 Let_def "Let s f == f(s)" |
181 Let_def "Let s f == f(s)" |
183 o_def "(f::'b=>'c) o g == (%(x::'a). f(g(x)))" |
|
184 if_def "If P x y == @z::'a. (P=True --> z=x) & (P=False --> z=y)" |
182 if_def "If P x y == @z::'a. (P=True --> z=x) & (P=False --> z=y)" |
185 |
183 |
186 (*arbitrary is completely unspecified, but is made to appear as a |
184 (*arbitrary is completely unspecified, but is made to appear as a |
187 definition syntactically*) |
185 definition syntactically*) |
188 arbitrary_def "False ==> arbitrary == (@x. False)" |
186 arbitrary_def "False ==> arbitrary == (@x. False)" |