changeset 35174 | e15040ae75d7 |
parent 25135 | 4f8176c940cf |
child 40002 | c5b5f7a3a3b1 |
35170:bb1d1c6a10bb | 35174:e15040ae75d7 |
---|---|
1 (* Title: HOLCF/ex/Fix2.thy |
1 (* Title: HOLCF/ex/Fix2.thy |
2 ID: $Id$ |
|
3 Author: Franz Regensburger |
2 Author: Franz Regensburger |
4 |
3 |
5 Show that fix is the unique least fixed-point operator. |
4 Show that fix is the unique least fixed-point operator. |
6 From axioms gix1_def,gix2_def it follows that fix = gix |
5 From axioms gix1_def,gix2_def it follows that fix = gix |
7 *) |
6 *) |