--- a/src/HOL/UNITY/WFair.ML Wed Aug 05 11:00:48 1998 +0200
+++ b/src/HOL/UNITY/WFair.ML Wed Aug 05 18:20:25 1998 +0200
@@ -325,6 +325,8 @@
(*** Proving the induction rules ***)
+(** The most general rule: r is any wf relation; f is any variant function **)
+
Goal "[| wf r; \
\ ALL m. leadsTo acts (A Int f-``{m}) \
\ ((A Int f-``(r^-1 ^^ {m})) Un B); \
@@ -355,7 +357,7 @@
Goal "[| wf r; \
\ ALL m:I. leadsTo acts (A Int f-``{m}) \
-\ ((A Int f-``(r^-1 ^^ {m})) Un B); \
+\ ((A Int f-``(r^-1 ^^ {m})) Un B); \
\ id: acts |] \
\ ==> leadsTo acts A ((A - (f-``I)) Un B)";
by (etac leadsTo_wf_induct 1);