(* Title: HOLCF/Plain_HOLCF.thy Author: Brian Huffman *) header {* Plain HOLCF *} theory Plain_HOLCF imports Cfun Sfun Cprod Sprod Ssum Up Discrete Lift One Tr Fix begin text {* Basic HOLCF concepts and types; does not include definition packages. *} end