equal
deleted
inserted
replaced
5 |
5 |
6 Basic definitions for the embedding of LCF into HOL. |
6 Basic definitions for the embedding of LCF into HOL. |
7 |
7 |
8 *) |
8 *) |
9 |
9 |
10 Holcfb = Nat + |
10 Holcfb = Nat |
|
11 |
|
12 (* + |
11 |
13 |
12 consts |
14 consts |
13 theleast :: "(nat=>bool)=>nat" |
15 theleast :: "(nat=>bool)=>nat" |
14 defs |
16 defs |
15 |
17 |
16 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)))" |
17 |
19 |
18 (* start 8bit 1 *) |
20 (* start |
19 (* end 8bit 1 *) |
21 8bit 1 *) |
|
22 |
|
23 syntax |
|
24 "Gmu" :: "[pttrn, bool] => nat" ("(3´_./ _)" 10) |
|
25 |
|
26 translations |
|
27 "´x.P" == "theleast(%x.P)" |
|
28 |
|
29 (* end |
|
30 8bit 1 *) |
20 |
31 |
21 end |
32 end |
|
33 *) |