--- a/src/HOL/Induct/Acc.ML Mon Jul 20 16:04:53 1998 +0200
+++ b/src/HOL/Induct/Acc.ML Mon Jul 20 16:19:49 1998 +0200
@@ -24,6 +24,15 @@
by (Fast_tac 1);
qed "acc_downward";
+Goal "(b,a) : r^* ==> a : acc r --> b : acc r";
+be rtrancl_induct 1;
+by(Blast_tac 1);
+ by(blast_tac (claset() addDs [acc_downward]) 1);
+val lemma = result();
+Goal "[| a : acc r; (b,a) : r^* |] ==> b : acc r";
+by(blast_tac (claset() addDs [lemma]) 1);
+qed "acc_downwards";
+
val [major,indhyp] = goal Acc.thy
"[| a : acc(r); \
\ !!x. [| x: acc(r); ALL y. (y,x):r --> P(y) |] ==> P(x) \