113 (Thy_Output.antiquotation @{binding lemma} |
113 (Thy_Output.antiquotation @{binding lemma} |
114 (Scan.lift (Scan.ahead Parse.not_eof) -- Args.prop -- |
114 (Scan.lift (Scan.ahead Parse.not_eof) -- Args.prop -- |
115 Scan.lift (Parse.position (Parse.reserved "by") -- Method.parse -- Scan.option Method.parse)) |
115 Scan.lift (Parse.position (Parse.reserved "by") -- Method.parse -- Scan.option Method.parse)) |
116 (fn {source, context = ctxt, ...} => fn ((prop_token, prop), (((_, by_pos), m1), m2)) => |
116 (fn {source, context = ctxt, ...} => fn ((prop_token, prop), (((_, by_pos), m1), m2)) => |
117 let |
117 let |
118 val prop_src = Token.src (Token.name_of_src source) [prop_token]; |
|
119 |
|
120 val reports = (by_pos, Markup.keyword1) :: maps Method.reports_of (m1 :: the_list m2); |
118 val reports = (by_pos, Markup.keyword1) :: maps Method.reports_of (m1 :: the_list m2); |
121 val _ = Context_Position.reports ctxt reports; |
119 val _ = Context_Position.reports ctxt reports; |
122 |
120 |
123 (* FIXME check proof!? *) |
121 (* FIXME check proof!? *) |
124 val _ = ctxt |
122 val _ = ctxt |
125 |> Proof.theorem NONE (K I) [[(prop, [])]] |
123 |> Proof.theorem NONE (K I) [[(prop, [])]] |
126 |> Proof.global_terminal_proof (m1, m2); |
124 |> Proof.global_terminal_proof (m1, m2); |
127 in |
125 in |
128 Thy_Output.output ctxt |
126 Thy_Output.output ctxt |
129 (Thy_Output.maybe_pretty_source Thy_Output.pretty_term ctxt prop_src [prop]) |
127 (Thy_Output.maybe_pretty_source |
|
128 Thy_Output.pretty_term ctxt [hd source, prop_token] [prop]) |
130 end)); |
129 end)); |
131 |
130 |
132 |
131 |
133 (* verbatim text *) |
132 (* verbatim text *) |
134 |
133 |