equal
deleted
inserted
replaced
205 by (rtac adm_all 1); |
205 by (rtac adm_all 1); |
206 by (rtac allI 1); |
206 by (rtac allI 1); |
207 by (rtac adm_eq 1); |
207 by (rtac adm_eq 1); |
208 by (cont_tacR 1); |
208 by (cont_tacR 1); |
209 by (rtac allI 1); |
209 by (rtac allI 1); |
210 by (stac strict_Rep_CFun1 1); |
210 by (stac Rep_CFun_strict1 1); |
211 by (rtac refl 1); |
211 by (rtac refl 1); |
212 by (Simp_tac 1); |
212 by (Simp_tac 1); |
213 by (rtac allI 1); |
213 by (rtac allI 1); |
214 by (res_inst_tac [("s","TT"),("t","b1$(iterate k g x)")] ssubst 1); |
214 by (res_inst_tac [("s","TT"),("t","b1$(iterate k g x)")] ssubst 1); |
215 by (etac spec 1); |
215 by (etac spec 1); |
230 by (rtac adm_all 1); |
230 by (rtac adm_all 1); |
231 by (rtac allI 1); |
231 by (rtac allI 1); |
232 by (rtac adm_eq 1); |
232 by (rtac adm_eq 1); |
233 by (cont_tacR 1); |
233 by (cont_tacR 1); |
234 by (rtac allI 1); |
234 by (rtac allI 1); |
235 by (stac strict_Rep_CFun1 1); |
235 by (stac Rep_CFun_strict1 1); |
236 by (rtac refl 1); |
236 by (rtac refl 1); |
237 by (rtac allI 1); |
237 by (rtac allI 1); |
238 by (Simp_tac 1); |
238 by (Simp_tac 1); |
239 by (res_inst_tac [("s","TT"),("t","b1$(iterate k g x)")] ssubst 1); |
239 by (res_inst_tac [("s","TT"),("t","b1$(iterate k g x)")] ssubst 1); |
240 by (etac spec 1); |
240 by (etac spec 1); |
259 by (rtac adm_all 1); |
259 by (rtac adm_all 1); |
260 by (rtac allI 1); |
260 by (rtac allI 1); |
261 by (rtac adm_eq 1); |
261 by (rtac adm_eq 1); |
262 by (cont_tacR 1); |
262 by (cont_tacR 1); |
263 by (rtac allI 1); |
263 by (rtac allI 1); |
264 by (stac strict_Rep_CFun1 1); |
264 by (stac Rep_CFun_strict1 1); |
265 by (rtac refl 1); |
265 by (rtac refl 1); |
266 by (rtac allI 1); |
266 by (rtac allI 1); |
267 by (Simp_tac 1); |
267 by (Simp_tac 1); |
268 by (res_inst_tac [("s","TT"),("t","b1$(iterate k g (x::'a))")] ssubst 1); |
268 by (res_inst_tac [("s","TT"),("t","b1$(iterate k g (x::'a))")] ssubst 1); |
269 by (etac spec 1); |
269 by (etac spec 1); |