1891 [REPEAT (eresolve_tac Abs_inverse_thms' 1), |
1891 [REPEAT (eresolve_tac Abs_inverse_thms' 1), |
1892 simp_tac (HOL_basic_ss addsimps [symmetric r]) 1, |
1892 simp_tac (HOL_basic_ss addsimps [symmetric r]) 1, |
1893 DEPTH_SOLVE_1 (ares_tac [prem] 1 ORELSE etac allE 1)])) |
1893 DEPTH_SOLVE_1 (ares_tac [prem] 1 ORELSE etac allE 1)])) |
1894 (prems ~~ constr_defs))])); |
1894 (prems ~~ constr_defs))])); |
1895 |
1895 |
1896 val case_names_induct = mk_case_names_induct descr; |
1896 val case_names_induct = mk_case_names_induct (List.concat descr'); |
1897 |
1897 |
1898 val (thy9, _) = thy8 |> |
1898 val (thy9, _) = thy8 |> |
1899 Theory.add_path big_name |> |
1899 Theory.add_path big_name |> |
1900 PureThy.add_thms [(("induct", dt_induct), [case_names_induct])] |>> |
1900 PureThy.add_thms [(("induct_weak", dt_induct), [case_names_induct])] |>> |
1901 Theory.parent_path |>>> |
1901 Theory.parent_path |>>> |
1902 DatatypeAux.store_thmss "distinct" new_type_names distinct_thms |>>> |
1902 DatatypeAux.store_thmss "distinct" new_type_names distinct_thms |>>> |
1903 DatatypeAux.store_thmss "constr_rep" new_type_names constr_rep_thmss |>>> |
1903 DatatypeAux.store_thmss "constr_rep" new_type_names constr_rep_thmss |>>> |
1904 DatatypeAux.store_thmss "perm" new_type_names perm_simps' |>>> |
1904 DatatypeAux.store_thmss "perm" new_type_names perm_simps' |>>> |
1905 DatatypeAux.store_thmss "inject" new_type_names inject_thms |>>> |
1905 DatatypeAux.store_thmss "inject" new_type_names inject_thms |>>> |