| changeset 4905 | be73ddff6c5a |
| child 17248 | 81bf91654e73 |
| 4904:5f6b2dd1cd11 | 4905:be73ddff6c5a |
|---|---|
1 |
|
2 val asms = goal thy "[| f(p) << p; !!q. f(q) << q ==> p << q |] ==> FIX(f)=p"; |
|
3 by (rewtac eq_def); |
|
4 by (rtac conjI 1); |
|
5 by (induct_tac "f" 1); |
|
6 by (rtac minimal 1); |
|
7 by (strip_tac 1); |
|
8 by (rtac less_trans 1); |
|
9 by (resolve_tac asms 2); |
|
10 by (etac less_ap_term 1); |
|
11 by (resolve_tac asms 1); |
|
12 by (rtac (FIX_eq RS eq_imp_less1) 1); |
|
13 qed "example"; |