| changeset 7681 | 4434adbe24a1 |
| parent 7453 | 18df56953792 |
| child 7721 | cb353d802ade |
--- a/src/HOL/Induct/Acc.ML Fri Oct 01 20:40:03 1999 +0200 +++ b/src/HOL/Induct/Acc.ML Fri Oct 01 20:41:58 1999 +0200 @@ -26,8 +26,8 @@ by (etac rtrancl_induct 1); by (Blast_tac 1); by (blast_tac (claset() addDs [acc_downward]) 1); +no_qed(); val lemma = result(); -no_qed(); Goal "[| a : acc r; (b,a) : r^* |] ==> b : acc r"; by (blast_tac (claset() addDs [lemma]) 1);