equal
deleted
inserted
replaced
339 |
339 |
340 val rec_o_maps = |
340 val rec_o_maps = |
341 fold_rev (curry (op @) o #co_rec_o_maps o the o #fp_co_induct_sugar) fp_sugars []; |
341 fold_rev (curry (op @) o #co_rec_o_maps o the o #fp_co_induct_sugar) fp_sugars []; |
342 |
342 |
343 val size_gen_o_map_thmss = |
343 val size_gen_o_map_thmss = |
344 if nested_size_gen_o_maps_complete then |
344 if nested_size_gen_o_maps_complete |
|
345 andalso forall (fn TFree (_, S) => S = @{sort type}) As then |
345 @{map 3} (fn goal => fn size_def => fn rec_o_map => |
346 @{map 3} (fn goal => fn size_def => fn rec_o_map => |
346 Goal.prove_sorry lthy2 [] [] goal (fn {context = ctxt, ...} => |
347 Goal.prove_sorry lthy2 [] [] goal (fn {context = ctxt, ...} => |
347 mk_size_gen_o_map_tac ctxt size_def rec_o_map all_inj_maps nested_size_maps) |
348 mk_size_gen_o_map_tac ctxt size_def rec_o_map all_inj_maps nested_size_maps) |
348 |> Thm.close_derivation |
349 |> Thm.close_derivation |
349 |> single) |
350 |> single) |