src/HOL/HOLCF/Plain_HOLCF.thy
author wenzelm
Sun Sep 18 20:33:48 2016 +0200 (2016-09-18)
changeset 63915 bab633745c7f
parent 62175 8ffc4d0e652d
child 65379 76a96e32bd23
permissions -rw-r--r--
tuned proofs;
wenzelm@42151
     1
(*  Title:      HOL/HOLCF/Plain_HOLCF.thy
huffman@40502
     2
    Author:     Brian Huffman
huffman@40502
     3
*)
huffman@40502
     4
wenzelm@62175
     5
section \<open>Plain HOLCF\<close>
huffman@40502
     6
huffman@40502
     7
theory Plain_HOLCF
huffman@40592
     8
imports Cfun Sfun Cprod Sprod Ssum Up Discrete Lift One Tr Fix
huffman@40502
     9
begin
huffman@40502
    10
wenzelm@62175
    11
text \<open>
huffman@40502
    12
  Basic HOLCF concepts and types; does not include definition packages.
wenzelm@62175
    13
\<close>
huffman@40502
    14
hoelzl@60040
    15
hide_const (open) Filter.principal
hoelzl@60040
    16
huffman@40502
    17
end