(* 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