| changeset 58880 | 0baae4311a9f |
| parent 55931 | 62156e694f3d |
| child 61169 | 4de9ff3ea29a |
--- a/src/HOL/HOLCF/Library/Option_Cpo.thy Sun Nov 02 17:14:15 2014 +0100 +++ b/src/HOL/HOLCF/Library/Option_Cpo.thy Sun Nov 02 17:16:01 2014 +0100 @@ -2,7 +2,7 @@ Author: Brian Huffman *) -header {* Cpo class instance for HOL option type *} +section {* Cpo class instance for HOL option type *} theory Option_Cpo imports HOLCF Sum_Cpo