added weak_coinduct_image

--- a/src/HOL/Gfp.ML	Thu May 31 16:07:35 2001 +0200
+++ b/src/HOL/Gfp.ML	Thu May 31 16:17:28 2001 +0200
@@ -42,6 +42,11 @@
 by Auto_tac;
 qed "weak_coinduct";
 
+Goal "!!X. [| a : X; g`X <= f (g`X) |] ==> g a : gfp f";
+by (etac (gfp_upperbound RS subsetD) 1);
+by (etac imageI 1);
+qed "weak_coinduct_image";
+
 Goal "[| X <= f(X Un gfp(f));  mono(f) |] ==>  \
 \    X Un gfp(f) <= f(X Un gfp(f))";
 by (blast_tac (claset() addDs [gfp_lemma2, mono_Un]) 1);