equal
deleted
inserted
replaced
35 {defs:thm list, elims:thm list, raw_induct:thm, induct:thm, |
35 {defs:thm list, elims:thm list, raw_induct:thm, induct:thm, |
36 intrs:thm list, |
36 intrs:thm list, |
37 mk_cases:thm list -> string -> thm, mono:thm, |
37 mk_cases:thm list -> string -> thm, mono:thm, |
38 unfold:thm} |
38 unfold:thm} |
39 val add_inductive : bool -> bool -> string list -> string list |
39 val add_inductive : bool -> bool -> string list -> string list |
40 -> thm list -> thm list -> theory -> theory * |
40 -> xstring list -> xstring list -> theory -> theory * |
41 {defs:thm list, elims:thm list, raw_induct:thm, induct:thm, |
41 {defs:thm list, elims:thm list, raw_induct:thm, induct:thm, |
42 intrs:thm list, |
42 intrs:thm list, |
43 mk_cases:thm list -> string -> thm, mono:thm, |
43 mk_cases:thm list -> string -> thm, mono:thm, |
44 unfold:thm} |
44 unfold:thm} |
45 end; |
45 end; |
598 (map_term_types (typ_subst_TVars_2 env)); |
598 (map_term_types (typ_subst_TVars_2 env)); |
599 val cs'' = map subst cs'; |
599 val cs'' = map subst cs'; |
600 val intr_ts'' = map subst intr_ts'; |
600 val intr_ts'' = map subst intr_ts'; |
601 |
601 |
602 in add_inductive_i verbose false "" coind false false cs'' intr_ts'' |
602 in add_inductive_i verbose false "" coind false false cs'' intr_ts'' |
603 monos con_defs thy |
603 (map (Attribute.thm_of) (PureThy.get_tthmss thy monos)) |
|
604 (map (Attribute.thm_of) (PureThy.get_tthmss thy con_defs)) thy |
604 end; |
605 end; |
605 |
606 |
606 end; |
607 end; |