| changeset 3718 | d78cf498a88c |
| parent 3563 | c4f13747489f |
| child 3768 | 67f4ac759100 |
--- a/src/HOL/NatDef.ML Fri Sep 26 10:12:04 1997 +0200 +++ b/src/HOL/NatDef.ML Fri Sep 26 10:21:14 1997 +0200 @@ -152,7 +152,7 @@ qed "nat_case_Suc"; goalw thy [wf_def, pred_nat_def] "wf(pred_nat)"; -by (strip_tac 1); +by (Clarify_tac 1); by (nat_ind_tac "x" 1); by (ALLGOALS Blast_tac); qed "wf_pred_nat";