author | wenzelm |
Tue, 09 Mar 1999 12:08:08 +0100 | |
changeset 6315 | ed71bedf6976 |
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";