| author | wenzelm |
| Tue, 16 Aug 2005 13:42:40 +0200 | |
| changeset 17069 | ee08b2466a09 |
| parent 4905 | be73ddff6c5a |
| child 17248 | 81bf91654e73 |
| permissions | -rw-r--r-- |
| 4905 | 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"; |