src/HOL/HOLCF/Plain_HOLCF.thy
author haftmann
Sun Jun 23 21:16:07 2013 +0200 (2013-06-23)
changeset 52435 6646bb548c6b
parent 42151 4da4fc77664b
child 58880 0baae4311a9f
permissions -rw-r--r--
migration from code_(const|type|class|instance) to code_printing and from code_module to code_identifier
     1 (*  Title:      HOL/HOLCF/Plain_HOLCF.thy
     2     Author:     Brian Huffman
     3 *)
     4 
     5 header {* Plain HOLCF *}
     6 
     7 theory Plain_HOLCF
     8 imports Cfun Sfun Cprod Sprod Ssum Up Discrete Lift One Tr Fix
     9 begin
    10 
    11 text {*
    12   Basic HOLCF concepts and types; does not include definition packages.
    13 *}
    14 
    15 end