added wf_converse_trancl, adapted proof of wfrec

--- 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";