equal
deleted
inserted
replaced
2217 Goal.prove_sorry lthy [] [] goal |
2217 Goal.prove_sorry lthy [] [] goal |
2218 (K (mk_map_tac m n cT unfold map_comp' map_cong0)) |
2218 (K (mk_map_tac m n cT unfold map_comp' map_cong0)) |
2219 |> Thm.close_derivation) |
2219 |> Thm.close_derivation) |
2220 goals cTs dtor_unfold_thms map_comp's map_cong0s; |
2220 goals cTs dtor_unfold_thms map_comp's map_cong0s; |
2221 in |
2221 in |
2222 map_split (fn thm => (thm RS @{thm pointfreeE}, thm)) maps |
2222 map_split (fn thm => (thm RS @{thm comp_eq_dest}, thm)) maps |
2223 end; |
2223 end; |
2224 |
2224 |
2225 val map_comp_thms = |
2225 val map_comp_thms = |
2226 let |
2226 let |
2227 val goal = fold_rev Logic.all (fs @ gs) |
2227 val goal = fold_rev Logic.all (fs @ gs) |