| changeset 25135 | 4f8176c940cf |
| parent 19742 | 86f21beabafc |
| child 35174 | e15040ae75d7 |
| 25134:3d4953e88449 | 25135:4f8176c940cf |
|---|---|
8 |
8 |
9 theory Fix2 |
9 theory Fix2 |
10 imports HOLCF |
10 imports HOLCF |
11 begin |
11 begin |
12 |
12 |
13 consts |
13 axiomatization |
14 gix :: "('a->'a)->'a" |
14 gix :: "('a->'a)->'a" where |
15 |
15 gix1_def: "F$(gix$F) = gix$F" and |
16 axioms |
|
17 gix1_def: "F$(gix$F) = gix$F" |
|
18 gix2_def: "F$y=y ==> gix$F << y" |
16 gix2_def: "F$y=y ==> gix$F << y" |
19 |
17 |
20 |
18 |
21 lemma lemma1: "fix = gix" |
19 lemma lemma1: "fix = gix" |
22 apply (rule ext_cfun) |
20 apply (rule ext_cfun) |