equal
deleted
inserted
replaced
379 ); |
379 ); |
380 |
380 |
381 fun gen_theorem schematic prep_att prep_stmt |
381 fun gen_theorem schematic prep_att prep_stmt |
382 kind before_qed after_qed (name, raw_atts) raw_elems raw_concl int lthy = |
382 kind before_qed after_qed (name, raw_atts) raw_elems raw_concl int lthy = |
383 let |
383 let |
384 val _ = Local_Theory.affirm lthy; |
384 val _ = Local_Theory.assert lthy; |
385 val thy = Proof_Context.theory_of lthy; |
385 val thy = Proof_Context.theory_of lthy; |
386 |
386 |
387 val attrib = prep_att thy; |
387 val attrib = prep_att thy; |
388 val elems = raw_elems |> map (Element.map_ctxt_attrib attrib); |
388 val elems = raw_elems |> map (Element.map_ctxt_attrib attrib); |
389 val ((more_atts, prems, stmt, facts), goal_ctxt) = |
389 val ((more_atts, prems, stmt, facts), goal_ctxt) = |