| changeset 4371 | 8755cdbbf6b3 |
| parent 4083 | bcff38832d89 |
| child 4793 | 03fd006fb97b |
| 4370:162abcd128a1 | 4371:8755cdbbf6b3 |
|---|---|
181 (* Misc Definitions *) |
181 (* Misc Definitions *) |
182 |
182 |
183 Let_def "Let s f == f(s)" |
183 Let_def "Let s f == f(s)" |
184 o_def "(f::'b=>'c) o g == (%(x::'a). f(g(x)))" |
184 o_def "(f::'b=>'c) o g == (%(x::'a). f(g(x)))" |
185 if_def "If P x y == @z::'a. (P=True --> z=x) & (P=False --> z=y)" |
185 if_def "If P x y == @z::'a. (P=True --> z=x) & (P=False --> z=y)" |
186 arbitrary_def "False ==> arbitrary == (@x. False)" |
|
186 |
187 |
187 |
188 |
188 end |
189 end |
189 |
190 |
190 |
191 |