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