equal
deleted
inserted
replaced
148 by (Clarify_tac 1); |
148 by (Clarify_tac 1); |
149 by (subgoal_tac "ALL n. nat_rec x (%i y. @z. z:Q & (z,y):r) n : Q" 1); |
149 by (subgoal_tac "ALL n. nat_rec x (%i y. @z. z:Q & (z,y):r) n : Q" 1); |
150 by (res_inst_tac[("x","nat_rec x (%i y. @z. z:Q & (z,y):r)")]exI 1); |
150 by (res_inst_tac[("x","nat_rec x (%i y. @z. z:Q & (z,y):r)")]exI 1); |
151 by (rtac allI 1); |
151 by (rtac allI 1); |
152 by (Simp_tac 1); |
152 by (Simp_tac 1); |
153 by (rtac someI2EX 1); |
153 by (rtac someI2_ex 1); |
154 by (Blast_tac 1); |
154 by (Blast_tac 1); |
155 by (Blast_tac 1); |
155 by (Blast_tac 1); |
156 by (rtac allI 1); |
156 by (rtac allI 1); |
157 by (induct_tac "n" 1); |
157 by (induct_tac "n" 1); |
158 by (Asm_simp_tac 1); |
158 by (Asm_simp_tac 1); |
159 by (Simp_tac 1); |
159 by (Simp_tac 1); |
160 by (rtac someI2EX 1); |
160 by (rtac someI2_ex 1); |
161 by (Blast_tac 1); |
161 by (Blast_tac 1); |
162 by (Blast_tac 1); |
162 by (Blast_tac 1); |
163 qed "wf_iff_no_infinite_down_chain"; |
163 qed "wf_iff_no_infinite_down_chain"; |
164 |
164 |
165 (*---------------------------------------------------------------------------- |
165 (*---------------------------------------------------------------------------- |