src/ZF/WF.ML
changeset 485 5e00a676a211
parent 443 10884e64c241
child 494 3686157a5a51
--- a/src/ZF/WF.ML	Tue Jul 26 13:21:20 1994 +0200
+++ b/src/ZF/WF.ML	Tue Jul 26 13:44:42 1994 +0200
@@ -95,7 +95,7 @@
 	   rename_last_tac a ["1"] (i+1),
 	   ares_tac prems i];
 
-(*The form of this rule is designed to match wfI2*)
+(*The form of this rule is designed to match wfI*)
 val wfr::amem::prems = goal WF.thy
     "[| wf(r);  a:A;  field(r)<=A;  \
 \       !!x.[| x: A;  ALL y. <y,x>: r --> P(y) |] ==> P(x) \
@@ -133,7 +133,7 @@
 \    ==>  wf(r)";
 by (rtac ([wf_onI2, subs] MRS (wf_on_subset_A RS wf_on_field_imp_wf)) 1);
 by (REPEAT (ares_tac [indhyp] 1));
-val wfI2 = result();
+val wfI = result();
 
 
 (*** Properties of well-founded relations ***)