added finite_acyclic_wf_converse

--- a/src/HOL/WF_Rel.ML	Mon Mar 23 13:56:53 1998 +0100
+++ b/src/HOL/WF_Rel.ML	Tue Mar 24 15:46:08 1998 +0100
@@ -117,6 +117,11 @@
 by (Asm_full_simp_tac 1);
 qed_spec_mp "finite_acyclic_wf";
 
+qed_goal "finite_acyclic_wf_converse" thy 
+ "ÄX. Ëfinite r; acyclic rÌ êë wf (r^-1)" (K [
+	etac (finite_converse RS iffD2 RS finite_acyclic_wf) 1,
+	etac (acyclic_converse RS iffD2) 1]);
+
 goal thy "!!r. finite r ==> wf r = acyclic r";
 by (blast_tac (claset() addIs [finite_acyclic_wf,wf_acyclic]) 1);
 qed "wf_iff_acyclic_if_finite";