changeset 243 | c22b85994e17 |
--- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/HOLCF/holcfb.thy Wed Jan 19 17:35:01 1994 +0100 @@ -0,0 +1,25 @@ +(* Title: HOLCF/holcfb.thy + ID: $Id$ + Author: Franz Regensburger + Copyright 1993 Technische Universitaet Muenchen + +Basic definitions for the embedding of LCF into HOL. + +*) + +Holcfb = Nat + + +consts + +theleast :: "(nat=>bool)=>nat" + +rules + +theleast_def "theleast(P) == (@z.(P(z) & (!n.P(n)-->z<=n)))" + +end + + + + +