equal
deleted
inserted
replaced
2043 rtac the1_equality 1, |
2043 rtac the1_equality 1, |
2044 solve rec_unique_thms prems 1, |
2044 solve rec_unique_thms prems 1, |
2045 resolve_tac rec_intrs 1, |
2045 resolve_tac rec_intrs 1, |
2046 REPEAT (solve (prems @ rec_total_thms) prems 1)]) |
2046 REPEAT (solve (prems @ rec_total_thms) prems 1)]) |
2047 end) (rec_eq_prems ~~ |
2047 end) (rec_eq_prems ~~ |
2048 Datatype_Prop.make_primrecs new_type_names descr' thy12); |
2048 Datatype_Prop.make_primrecs reccomb_names descr' thy12); |
2049 |
2049 |
2050 val dt_infos = map_index (make_dt_info pdescr induct reccomb_names rec_thms) |
2050 val dt_infos = map_index (make_dt_info pdescr induct reccomb_names rec_thms) |
2051 (descr1 ~~ distinct_thms ~~ inject_thms); |
2051 (descr1 ~~ distinct_thms ~~ inject_thms); |
2052 |
2052 |
2053 (* FIXME: theorems are stored in database for testing only *) |
2053 (* FIXME: theorems are stored in database for testing only *) |