# HG changeset patch
# User nipkow
# Date 900944389 -7200
# Node ID c0e18afae4336e5b838e16c55f3084f4a9a2b553
# Parent  53e505c6019cb599e47279b7be9d9a249e056ff8
Added acc_downwards

diff -r 53e505c6019c -r c0e18afae433 src/HOL/Induct/Acc.ML
--- 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) \