src/HOLCF/fun3.ML
author lcp
Tue, 16 Aug 1994 19:09:43 +0200
changeset 536 5fbfa997f1b0
parent 243 c22b85994e17
permissions -rw-r--r--
ZF/domrange/domain_of_prod, domain_empty, etc: moved to equalities.ML where they can be proved trivially using eq_cs ZF/domrange/XXX_empty: renamed XXX_0

(*  Title: 	HOLCF/fun3.ML
    ID:         $Id$
    Author: 	Franz Regensburger
    Copyright   1993 Technische Universitaet Muenchen
*)

open Fun3;