equal
deleted
inserted
replaced
1 (* Title: HOL/HOLCF/Plain_HOLCF.thy |
1 (* Title: HOL/HOLCF/Plain_HOLCF.thy |
2 Author: Brian Huffman |
2 Author: Brian Huffman |
3 *) |
3 *) |
4 |
4 |
5 section {* Plain HOLCF *} |
5 section \<open>Plain HOLCF\<close> |
6 |
6 |
7 theory Plain_HOLCF |
7 theory Plain_HOLCF |
8 imports Cfun Sfun Cprod Sprod Ssum Up Discrete Lift One Tr Fix |
8 imports Cfun Sfun Cprod Sprod Ssum Up Discrete Lift One Tr Fix |
9 begin |
9 begin |
10 |
10 |
11 text {* |
11 text \<open> |
12 Basic HOLCF concepts and types; does not include definition packages. |
12 Basic HOLCF concepts and types; does not include definition packages. |
13 *} |
13 \<close> |
14 |
14 |
15 hide_const (open) Filter.principal |
15 hide_const (open) Filter.principal |
16 |
16 |
17 end |
17 end |