changeset 40502 | 8e92772bc0e8 |
child 40592 | f432973ce0f6 |
--- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/HOLCF/Plain_HOLCF.thy Wed Nov 10 17:56:08 2010 -0800 @@ -0,0 +1,15 @@ +(* Title: HOLCF/Plain_HOLCF.thy + Author: Brian Huffman +*) + +header {* Plain HOLCF *} + +theory Plain_HOLCF +imports Cfun Cprod Sprod Ssum Up Discrete Lift One Tr Fix +begin + +text {* + Basic HOLCF concepts and types; does not include definition packages. +*} + +end