equal
deleted
inserted
replaced
1122 fun after_qed thm_name thms lthy = |
1122 fun after_qed thm_name thms lthy = |
1123 Local_Theory.note (thm_name, (flat thms)) lthy |> snd |
1123 Local_Theory.note (thm_name, (flat thms)) lthy |> snd |
1124 |
1124 |
1125 fun setup_proof (thm_name, src) lthy = |
1125 fun setup_proof (thm_name, src) lthy = |
1126 let |
1126 let |
1127 val text = Input.source_content src |
1127 val (text, _) = Input.source_content src |
1128 val trm = Code_Runtime.value lthy result_cookie ("", text) |
1128 val trm = Code_Runtime.value lthy result_cookie ("", text) |
1129 in |
1129 in |
1130 Proof.theorem NONE (after_qed thm_name) [[(trm, [])]] lthy |
1130 Proof.theorem NONE (after_qed thm_name) [[(trm, [])]] lthy |
1131 end |
1131 end |
1132 |
1132 |