equal
deleted
inserted
replaced
1572 (fn {context = ctxt, prems} => |
1572 (fn {context = ctxt, prems} => |
1573 mk_set_cases_tac ctxt (certify ctxt ta) prems exhaust set_thms) |
1573 mk_set_cases_tac ctxt (certify ctxt ta) prems exhaust set_thms) |
1574 |> singleton (Proof_Context.export names_lthy lthy) |
1574 |> singleton (Proof_Context.export names_lthy lthy) |
1575 |> Thm.close_derivation |
1575 |> Thm.close_derivation |
1576 |> rotate_prems ~1; |
1576 |> rotate_prems ~1; |
|
1577 |
|
1578 val consumes_attr = Attrib.internal (K (Rule_Cases.consumes 1)); |
|
1579 val cases_set_attr = |
|
1580 Attrib.internal (K (Induct.cases_pred (name_of_set set))); |
1577 in |
1581 in |
1578 (thm, [](* TODO: [@{attributes [elim?]}, |
1582 (* TODO: @{attributes [elim?]} *) |
1579 Attrib.internal (K (Induct.cases_pred (name_of_set set)))] *)) |
1583 (thm, [consumes_attr, cases_set_attr]) |
1580 end) setAs) |
1584 end) setAs) |
1581 end; |
1585 end; |
1582 |
1586 |
1583 val set_intros_thms = |
1587 val set_intros_thms = |
1584 let |
1588 let |