author | wenzelm |
Wed, 13 Jan 2016 23:07:06 +0100 | |
changeset 62175 | 8ffc4d0e652d |
parent 60040 | 1fa1023b13b9 |
child 65379 | 76a96e32bd23 |
permissions | -rw-r--r-- |
(* Title: HOL/HOLCF/Plain_HOLCF.thy Author: Brian Huffman *) section \<open>Plain HOLCF\<close> theory Plain_HOLCF imports Cfun Sfun Cprod Sprod Ssum Up Discrete Lift One Tr Fix begin text \<open> Basic HOLCF concepts and types; does not include definition packages. \<close> hide_const (open) Filter.principal end