equal
deleted
inserted
replaced
1 (* Title: HOLCF/holcfb.thy |
1 (* Title: HOLCF/holcfb.thy |
2 ID: $Id$ |
2 ID: $Id$ |
3 Author: Franz Regensburger |
3 Author: Franz Regensburger |
4 Copyright 1993 Technische Universitaet Muenchen |
4 Copyright 1993 Technische Universitaet Muenchen |
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 |
11 |
12 consts |
12 consts |
13 theleast :: "(nat=>bool)=>nat" |
13 theleast :: "(nat=>bool)=>nat" |
14 defs |
14 defs |
15 |
15 |
16 theleast_def "theleast P == (@z.(P z & (!n.P n --> z<=n)))" |
16 theleast_def "theleast P == (@z.(P z & (!n.P n --> z<=n)))" |
17 |
17 |
18 (* start 8bit 1 *) |
18 (* start 8bit 1 *) |