| changeset 6301 | 08245f5a436d |
| parent 5618 | 721671c68324 |
| child 7453 | 18df56953792 |
--- a/src/HOL/Induct/Acc.ML Wed Mar 03 11:12:29 1999 +0100 +++ b/src/HOL/Induct/Acc.ML Wed Mar 03 11:15:18 1999 +0100 @@ -45,7 +45,7 @@ Goal "!x. x : acc(r) ==> wf(r)"; by (rtac wfUNIVI 1); -by(deepen_tac (claset() addEs [acc_induct]) 1 1); +by (deepen_tac (claset() addEs [acc_induct]) 1 1); qed "acc_wfI"; Goal "wf(r) ==> x : acc(r)";