# HG changeset patch
# User oheimb
# Date 891284885 -7200
# Node ID afebaa81f14881ad3ac6d9d8f5da5ee1bc59e264
# Parent  1681b32dd13488177e73e7afd7db61f761981cc8
added wf_converse_trancl, adapted proof of wfrec

diff -r 1681b32dd134 -r afebaa81f148 src/HOL/WF.ML
--- a/src/HOL/WF.ML	Mon Mar 30 21:06:09 1998 +0200
+++ b/src/HOL/WF.ML	Mon Mar 30 21:08:05 1998 +0200
@@ -63,6 +63,11 @@
 qed "wf_trancl";
 
 
+val wf_converse_trancl = prove_goal thy 
+"!!X. wf (r^-1) ==> wf ((r^+)^-1)" (K [
+	stac (trancl_converse RS sym) 1,
+	etac wf_trancl 1]);
+
 (*----------------------------------------------------------------------------
  * Minimal-element characterization of well-foundedness
  *---------------------------------------------------------------------------*)
@@ -285,10 +290,10 @@
 by (rtac trans_trancl 1);
 by (rtac transD 1);
 by (rtac trans_trancl 1);
-by (forw_inst_tac [("a","ya")] r_into_trancl 1);
+by (forw_inst_tac [("p","(ya,y)")] r_into_trancl 1);
 by (atac 1);
 by (atac 1);
-by (forw_inst_tac [("a","ya")] r_into_trancl 1);
+by (forw_inst_tac [("p","(ya,y)")] r_into_trancl 1);
 by (atac 1);
 qed "wfrec";