(* Title: HOLCF/HOLCF.thy ID: $Id$ Author: Franz Regensburger License: GPL (GNU GENERAL PUBLIC LICENSE) Top theory for HOLCF system. *) HOLCF = Sprod3 + Ssum3 + Up3 + Lift + Discrete + One + Tr