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