src/HOLCF/Plain_HOLCF.thy
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