changeset 19755 | 90f80de04c46 |
parent 19754 | 489e6be0b19d |
child 19756 | 61c4117345c6 |
--- a/src/LCF/ex/Ex4.ML Thu Jun 01 14:54:44 2006 +0200 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,15 +0,0 @@ - -(* $Id$ *) - -val asms = goal (the_context ()) "[| 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";