equal
deleted
inserted
replaced
1381 rtac trans_fun_cong_image_id_id_apply, atac]) |
1381 rtac trans_fun_cong_image_id_id_apply, atac]) |
1382 (drop m set_naturals)]) |
1382 (drop m set_naturals)]) |
1383 (map_wpulls ~~ (pickWP_assms_tacs ~~ set_naturalss)) 1; |
1383 (map_wpulls ~~ (pickWP_assms_tacs ~~ set_naturalss)) 1; |
1384 |
1384 |
1385 fun mk_mor_thePull_nth_tac conv pick m mor_def map_wpulls map_comps pickWP_assms_tacs |
1385 fun mk_mor_thePull_nth_tac conv pick m mor_def map_wpulls map_comps pickWP_assms_tacs |
1386 {context = ctxt, prems = _} = |
1386 {context = ctxt, prems = _: thm list} = |
1387 let |
1387 let |
1388 val n = length map_comps; |
1388 val n = length map_comps; |
1389 in |
1389 in |
1390 unfold_thms_tac ctxt [mor_def] THEN |
1390 unfold_thms_tac ctxt [mor_def] THEN |
1391 EVERY' [rtac conjI, |
1391 EVERY' [rtac conjI, |