changeset 35794 | 8cd7134275cc |
parent 35055 | f0ecf952b864 |
child 35915 | 5ea16bc10a7a |
35793:950d098c4a12 | 35794:8cd7134275cc |
---|---|
1 (* Title: HOLCF/Fix.thy |
1 (* Title: HOLCF/Fix.thy |
2 Author: Franz Regensburger |
2 Author: Franz Regensburger |
3 Author: Brian Huffman |
|
3 *) |
4 *) |
4 |
5 |
5 header {* Fixed point operator and admissibility *} |
6 header {* Fixed point operator and admissibility *} |
6 |
7 |
7 theory Fix |
8 theory Fix |