equal
deleted
inserted
replaced
3 Copyright : 1998 University of Cambridge |
3 Copyright : 1998 University of Cambridge |
4 Description : *-transforms |
4 Description : *-transforms |
5 *) |
5 *) |
6 |
6 |
7 (*-------------------------------------------------------- |
7 (*-------------------------------------------------------- |
8 Preamble - Pulling "?" over "!" |
8 Preamble - Pulling "EX" over "ALL" |
9 ---------------------------------------------------------*) |
9 ---------------------------------------------------------*) |
10 |
10 |
11 (* This proof does not need AC and was suggested by the |
11 (* This proof does not need AC and was suggested by the |
12 referee for the JCM Paper: let f(x) be least y such |
12 referee for the JCM Paper: let f(x) be least y such |
13 that Q(x,y) |
13 that Q(x,y) |