src/HOL/HOLCF/Plain_HOLCF.thy
author hoelzl
Sun Apr 12 11:34:09 2015 +0200 (2015-04-12)
changeset 60040 1fa1023b13b9
parent 58880 0baae4311a9f
child 62175 8ffc4d0e652d
permissions -rw-r--r--
move MOST and INFM in Infinite_Set to Filter; change them to abbreviations over the cofinite filter
     1 (*  Title:      HOL/HOLCF/Plain_HOLCF.thy
     2     Author:     Brian Huffman
     3 *)
     4 
     5 section {* 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 hide_const (open) Filter.principal
    16 
    17 end