| changeset 243 | c22b85994e17 |
| child 1168 | 74be52691d62 |
| 242:8fe3e66abf0c | 243:c22b85994e17 |
|---|---|
1 (* Title: HOLCF/holcfb.thy |
|
2 ID: $Id$ |
|
3 Author: Franz Regensburger |
|
4 Copyright 1993 Technische Universitaet Muenchen |
|
5 |
|
6 Basic definitions for the embedding of LCF into HOL. |
|
7 |
|
8 *) |
|
9 |
|
10 Holcfb = Nat + |
|
11 |
|
12 consts |
|
13 |
|
14 theleast :: "(nat=>bool)=>nat" |
|
15 |
|
16 rules |
|
17 |
|
18 theleast_def "theleast(P) == (@z.(P(z) & (!n.P(n)-->z<=n)))" |
|
19 |
|
20 end |
|
21 |
|
22 |
|
23 |
|
24 |
|
25 |