author | wenzelm |
Mon, 17 Oct 2005 23:10:16 +0200 | |
changeset 17878 | 5b9efe4d6b47 |
parent 17248 | 81bf91654e73 |
permissions | -rw-r--r-- |
17878 | 1 |
|
2 |
(* $Id$ *) |
|
4905 | 3 |
|
17248 | 4 |
val asms = goal (the_context ()) "[| f(p) << p; !!q. f(q) << q ==> p << q |] ==> FIX(f)=p"; |
4905 | 5 |
by (rewtac eq_def); |
6 |
by (rtac conjI 1); |
|
7 |
by (induct_tac "f" 1); |
|
8 |
by (rtac minimal 1); |
|
9 |
by (strip_tac 1); |
|
10 |
by (rtac less_trans 1); |
|
11 |
by (resolve_tac asms 2); |
|
12 |
by (etac less_ap_term 1); |
|
13 |
by (resolve_tac asms 1); |
|
14 |
by (rtac (FIX_eq RS eq_imp_less1) 1); |
|
15 |
qed "example"; |