| changeset 58880 | 0baae4311a9f |
| parent 44066 | d74182c93f04 |
| child 61424 | c3658c18b7bc |
| 58879:143c85e3cdb5 | 58880:0baae4311a9f |
|---|---|
1 (* Title: HOL/HOLCF/Fix.thy |
1 (* Title: HOL/HOLCF/Fix.thy |
2 Author: Franz Regensburger |
2 Author: Franz Regensburger |
3 Author: Brian Huffman |
3 Author: Brian Huffman |
4 *) |
4 *) |
5 |
5 |
6 header {* Fixed point operator and admissibility *} |
6 section {* Fixed point operator and admissibility *} |
7 |
7 |
8 theory Fix |
8 theory Fix |
9 imports Cfun |
9 imports Cfun |
10 begin |
10 begin |
11 |
11 |