| changeset 58880 | 0baae4311a9f |
| parent 42151 | 4da4fc77664b |
| child 60040 | 1fa1023b13b9 |
--- a/src/HOL/HOLCF/Plain_HOLCF.thy Sun Nov 02 17:14:15 2014 +0100 +++ b/src/HOL/HOLCF/Plain_HOLCF.thy Sun Nov 02 17:16:01 2014 +0100 @@ -2,7 +2,7 @@ Author: Brian Huffman *) -header {* Plain HOLCF *} +section {* Plain HOLCF *} theory Plain_HOLCF imports Cfun Sfun Cprod Sprod Ssum Up Discrete Lift One Tr Fix