equal
deleted
inserted
replaced
304 apply (induct_tac "l") |
304 apply (induct_tac "l") |
305 apply (simp) |
305 apply (simp) |
306 apply (metis) |
306 apply (metis) |
307 done |
307 done |
308 |
308 |
|
309 ML {* (atomize_thm @{thm list_induct_hol4}) *} |
|
310 |
|
311 ML {* regularise (prop_of (atomize_thm @{thm list_induct_hol4})) @{typ "'a list"} @{term "op \<approx>"} @{context} *} |
|
312 |
309 prove list_induct_r: {* |
313 prove list_induct_r: {* |
310 build_regularize_goal (atomize_thm @{thm list_induct_hol4}) @{typ "'a List.list"} @{term "op \<approx>"} @{context} *} |
314 build_regularize_goal (atomize_thm @{thm list_induct_hol4}) @{typ "'a list"} @{term "op \<approx>"} @{context} *} |
311 apply (simp only: equiv_res_forall[OF equiv_list_eq]) |
315 apply (simp only: equiv_res_forall[OF equiv_list_eq]) |
312 thm RIGHT_RES_FORALL_REGULAR |
316 thm RIGHT_RES_FORALL_REGULAR |
313 apply (rule RIGHT_RES_FORALL_REGULAR) |
317 apply (rule RIGHT_RES_FORALL_REGULAR) |
314 prefer 2 |
318 prefer 2 |
315 apply (assumption) |
319 apply (assumption) |