| changeset 58880 | 0baae4311a9f |
| parent 49759 | ecf1d5d87e5e |
| child 62175 | 8ffc4d0e652d |
| 58879:143c85e3cdb5 | 58880:0baae4311a9f |
|---|---|
1 (* Title: HOL/HOLCF/Fixrec.thy |
1 (* Title: HOL/HOLCF/Fixrec.thy |
2 Author: Amber Telfer and Brian Huffman |
2 Author: Amber Telfer and Brian Huffman |
3 *) |
3 *) |
4 |
4 |
5 header "Package for defining recursive functions in HOLCF" |
5 section "Package for defining recursive functions in HOLCF" |
6 |
6 |
7 theory Fixrec |
7 theory Fixrec |
8 imports Plain_HOLCF |
8 imports Plain_HOLCF |
9 keywords "fixrec" :: thy_decl |
9 keywords "fixrec" :: thy_decl |
10 begin |
10 begin |