equal
deleted
inserted
replaced
533 DEPTH_SOLVE_1 (ares_tac [prem] 1)])) |
533 DEPTH_SOLVE_1 (ares_tac [prem] 1)])) |
534 (prems ~~ (constr_defs @ (map mk_meta_eq iso_char_thms))))]); |
534 (prems ~~ (constr_defs @ (map mk_meta_eq iso_char_thms))))]); |
535 |
535 |
536 val thy7 = thy6 |> |
536 val thy7 = thy6 |> |
537 Theory.add_path big_name |> |
537 Theory.add_path big_name |> |
538 PureThy.add_tthms [(("induct", Attribute.tthm_of dt_induct), [])] |> |
538 PureThy.add_thms [(("induct", dt_induct), [])] |> |
539 Theory.parent_path; |
539 Theory.parent_path; |
540 |
540 |
541 in (thy7, constr_inject, dist_rewrites, dt_induct) |
541 in (thy7, constr_inject, dist_rewrites, dt_induct) |
542 end; |
542 end; |
543 |
543 |