# HG changeset patch
# User oheimb
# Date 890750768 -3600
# Node ID 35b47e36e6151f87503c0de711d6c157ba3f72dc
# Parent  2b8ead8e9393bcbd50604d0f678ebdbe27bb8d7f
added finite_acyclic_wf_converse

diff -r 2b8ead8e9393 -r 35b47e36e615 src/HOL/WF_Rel.ML
--- 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";