equal
deleted
inserted
replaced
150 goalw thy [nat_case_def] "nat_case a f (Suc k) = f(k)"; |
150 goalw thy [nat_case_def] "nat_case a f (Suc k) = f(k)"; |
151 by (blast_tac (!claset addIs [select_equality]) 1); |
151 by (blast_tac (!claset addIs [select_equality]) 1); |
152 qed "nat_case_Suc"; |
152 qed "nat_case_Suc"; |
153 |
153 |
154 goalw thy [wf_def, pred_nat_def] "wf(pred_nat)"; |
154 goalw thy [wf_def, pred_nat_def] "wf(pred_nat)"; |
155 by (strip_tac 1); |
155 by (Clarify_tac 1); |
156 by (nat_ind_tac "x" 1); |
156 by (nat_ind_tac "x" 1); |
157 by (ALLGOALS Blast_tac); |
157 by (ALLGOALS Blast_tac); |
158 qed "wf_pred_nat"; |
158 qed "wf_pred_nat"; |
159 |
159 |
160 |
160 |