--- a/src/HOL/Induct/Acc.ML Tue Jul 21 08:54:09 1998 +0200
+++ b/src/HOL/Induct/Acc.ML Tue Jul 21 12:12:52 1998 +0200
@@ -25,12 +25,12 @@
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);
+by (etac 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);
+by (blast_tac (claset() addDs [lemma]) 1);
qed "acc_downwards";
val [major,indhyp] = goal Acc.thy