(* Title: HOL/HOLCF/Plain_HOLCF.thy Author: Brian Huffman *) section ‹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. › hide_const (open) Filter.principal end