src/HOLCF/explicit_domains/README
author oheimb
Wed, 18 Dec 1996 15:16:13 +0100
changeset 2445 51993fea433f
parent 1274 ea0668a1c0ba
permissions -rw-r--r--
removed Holcfb.thy and Holcfb.ML, moving classical3 to HOL.ML as classical2

(*
    ID:         $Id$
    Author: 	Franz Regensburger
    Copyright   1995 Technische Universitaet Muenchen

*)

The files contained in this directory are examples for the
explicit construction of domains. The technique used is described
in the thesis

	HOLCF: Eine konservative Erweiterung von HOL um LCF

The thesis is available via the web using URL

	http://www4.informatik.tu-muenchen.de/~regensbu/papers.html


The same construction is automatically performed if you use the
type definition package of David Oheimb. See subdirectory HOLCF/domains
for more details.