author | wenzelm |
Tue, 06 Sep 2005 19:28:58 +0200 | |
changeset 17291 | 94f6113fe9ed |
parent 14981 | e73f8140af78 |
child 18075 | 43000d7a017c |
permissions | -rw-r--r-- |
1461 | 1 |
(* Title: HOLCF/ex/Fix2.ML |
1274 | 2 |
ID: $Id$ |
1461 | 3 |
Author: Franz Regensburger |
1274 | 4 |
*) |
5 |
||
9265 | 6 |
Goal "fix = gix"; |
7 |
by (rtac ext_cfun 1); |
|
8 |
by (rtac antisym_less 1); |
|
9 |
by (rtac fix_least 1); |
|
10 |
by (rtac gix1_def 1); |
|
11 |
by (rtac gix2_def 1); |
|
12 |
by (rtac (fix_eq RS sym) 1); |
|
13 |
qed "lemma1"; |
|
1274 | 14 |
|
15 |
||
10835 | 16 |
Goal "gix$F=lub(range(%i. iterate i F UU))"; |
9265 | 17 |
by (rtac (lemma1 RS subst) 1); |
18 |
by (rtac fix_def2 1); |
|
19 |
qed "lemma2"; |