equal
deleted
inserted
replaced
294 |> map prop_of |
294 |> map prop_of |
295 |> map Logic.strip_horn |
295 |> map Logic.strip_horn |
296 |> split_list |
296 |> split_list |
297 |>> (map o map) strip_params_prems_concl |
297 |>> (map o map) strip_params_prems_concl |
298 |
298 |
299 val prems = map2 (process_ecase lthy'' c) (flat ecases) (flat bclausesss) |
299 val premss = ((map2 o map2) (process_ecase lthy'' c) ecases bclausesss) |
|
300 |
300 in |
301 in |
301 Goal.prove_multi lthy'' [] prems main_concls |
302 map2 (fn (prems, bclausess) => fn (exh, concl) => |
302 (fn {prems:thm list, context} => |
303 Goal.prove lthy'' [] prems concl |
303 let |
304 (fn {prems: thm list, context} => |
304 val prems' = partitions prems (map length bclausesss) |
305 HEADGOAL (case_tac context c bn_finite_thms eq_iff_thms bn_eqvt permute_bns perm_bn_alphas |
305 in |
306 (prems, bclausess) exh) |
306 EVERY1 [Goal.conjunction_tac, |
307 ) |
307 RANGE (map2 (case_tac context c bn_finite_thms eq_iff_thms bn_eqvt permute_bns perm_bn_alphas) |
308 ) (premss ~~ bclausesss) (exhausts' ~~ main_concls) |
308 (prems' ~~ bclausesss) exhausts')] |
309 |> ProofContext.export lthy'' lthy |
309 end) |
|
310 |> ProofContext.export lthy'' lthy |
|
311 end |
310 end |
312 *} |
311 *} |
313 |
312 |
314 |
313 |
315 |
314 |