equal
deleted
inserted
replaced
303 @{thms ho_memb_rsp ho_cons_rsp ho_card1_rsp ho_map_rsp ho_append_rsp ho_fold_rsp} |
303 @{thms ho_memb_rsp ho_cons_rsp ho_card1_rsp ho_map_rsp ho_append_rsp ho_fold_rsp} |
304 @ @{thms ho_all_prs ho_ex_prs} *} |
304 @ @{thms ho_all_prs ho_ex_prs} *} |
305 |
305 |
306 ML {* fun lift_thm_fset lthy t = lift_thm lthy qty "fset" rsp_thms defs t *} |
306 ML {* fun lift_thm_fset lthy t = lift_thm lthy qty "fset" rsp_thms defs t *} |
307 |
307 |
|
308 thm m2 |
|
309 |
|
310 thm append_assoc |
308 (* ML {* lift_thm_fset @{context} @{thm neq_Nil_conv} *} *) |
311 (* ML {* lift_thm_fset @{context} @{thm neq_Nil_conv} *} *) |
309 ML {* lift_thm_fset @{context} @{thm m1} *} |
312 ML {* lift_thm_fset @{context} @{thm m1} *} |
310 ML {* lift_thm_fset @{context} @{thm m2} *} |
313 ML {* lift_thm_fset @{context} @{thm m2} *} |
311 ML {* lift_thm_fset @{context} @{thm list_eq.intros(4)} *} |
314 ML {* lift_thm_fset @{context} @{thm list_eq.intros(4)} *} |
312 ML {* lift_thm_fset @{context} @{thm list_eq.intros(5)} *} |
315 ML {* lift_thm_fset @{context} @{thm list_eq.intros(5)} *} |