author | wenzelm |
Fri, 15 May 1998 11:34:12 +0200 | |
changeset 4932 | c90411dde8e8 |
parent 4905 | be73ddff6c5a |
child 17248 | 81bf91654e73 |
permissions | -rw-r--r-- |
val asms = goal thy "[| f(p) << p; !!q. f(q) << q ==> p << q |] ==> FIX(f)=p"; by (rewtac eq_def); by (rtac conjI 1); by (induct_tac "f" 1); by (rtac minimal 1); by (strip_tac 1); by (rtac less_trans 1); by (resolve_tac asms 2); by (etac less_ap_term 1); by (resolve_tac asms 1); by (rtac (FIX_eq RS eq_imp_less1) 1); qed "example";