changeset 40774 | 0437dbc127b3 |
parent 40592 | f432973ce0f6 |
child 42151 | 4da4fc77664b |
--- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/HOL/HOLCF/Plain_HOLCF.thy Sat Nov 27 16:08:10 2010 -0800 @@ -0,0 +1,15 @@ +(* Title: HOLCF/Plain_HOLCF.thy + Author: Brian Huffman +*) + +header {* 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. +*} + +end