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