changeset 1168 | 74be52691d62 |
parent 243 | c22b85994e17 |
child 1274 | ea0668a1c0ba |
1167:cbd32a0f2f41 | 1168:74be52691d62 |
---|---|
11 |
11 |
12 consts |
12 consts |
13 |
13 |
14 theleast :: "(nat=>bool)=>nat" |
14 theleast :: "(nat=>bool)=>nat" |
15 |
15 |
16 rules |
16 defs |
17 |
17 |
18 theleast_def "theleast(P) == (@z.(P(z) & (!n.P(n)-->z<=n)))" |
18 theleast_def "theleast P == (@z.(P z & (!n.P n --> z<=n)))" |
19 |
19 |
20 end |
20 end |
21 |
21 |
22 |
22 |
23 |
23 |