src/HOLCF/HOLCF.ML
author paulson
Wed, 23 Jul 1997 11:52:22 +0200
changeset 3564 f886dbd91ee5
parent 2355 ee9bdbe2ac8a
child 3661 1ea4a45b9412
permissions -rw-r--r--
Now Datatype.occs_in_prems prints the necessary warning ITSELF. It is also easier to invoke and even works if the induction variable is a parameter (rather than a free variable).

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

open HOLCF;

val HOLCF_ss = !simpset;