(* 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.*}hide_const (open) Filter.principalend