33 |
33 |
34 |
34 |
35 (* fact references *) |
35 (* fact references *) |
36 |
36 |
37 fun thm_antiq kind scan = ML_Context.add_antiq kind |
37 fun thm_antiq kind scan = ML_Context.add_antiq kind |
38 (scan >> (fn ths => fn {struct_name, background} => |
38 (fn _ => scan >> (fn ths => fn {struct_name, background} => |
39 let |
39 let |
40 val i = serial (); |
40 val i = serial (); |
41 val (a, background') = background |
41 val (a, background') = background |
42 |> ML_Antiquote.variant kind ||> put_thms (i, ths); |
42 |> ML_Antiquote.variant kind ||> put_thms (i, ths); |
43 val ml = (thm_bind kind a i, struct_name ^ "." ^ a); |
43 val ml = (thm_bind kind a i, struct_name ^ "." ^ a); |
51 |
51 |
52 val by = Args.$$$ "by"; |
52 val by = Args.$$$ "by"; |
53 val goal = Scan.unless (Scan.lift by) Args.prop; |
53 val goal = Scan.unless (Scan.lift by) Args.prop; |
54 |
54 |
55 val _ = ML_Context.add_antiq "lemma" |
55 val _ = ML_Context.add_antiq "lemma" |
56 (Args.context -- Args.mode "open" -- Scan.repeat1 goal -- |
56 (fn pos => Args.context -- Args.mode "open" -- Scan.repeat1 goal -- |
57 Scan.lift (by |-- Method.parse -- Scan.option Method.parse) >> |
57 Scan.lift (by |-- Method.parse -- Scan.option Method.parse) >> |
58 (fn (((ctxt, is_open), props), methods) => fn {struct_name, background} => |
58 (fn (((ctxt, is_open), props), methods) => fn {struct_name, background} => |
59 let |
59 let |
60 val i = serial (); |
60 val i = serial (); |
61 val prep_result = Goal.norm_result #> not is_open ? Thm.close_derivation; |
61 val prep_result = |
|
62 Goal.norm_result #> Thm.default_position pos #> not is_open ? Thm.close_derivation; |
62 fun after_qed [res] goal_ctxt = |
63 fun after_qed [res] goal_ctxt = |
63 put_thms (i, map prep_result (ProofContext.export goal_ctxt ctxt res)) goal_ctxt; |
64 put_thms (i, map prep_result (ProofContext.export goal_ctxt ctxt res)) goal_ctxt; |
64 val ctxt' = ctxt |
65 val ctxt' = ctxt |
65 |> Proof.theorem_i NONE after_qed [map (rpair []) props] |
66 |> Proof.theorem_i NONE after_qed [map (rpair []) props] |
66 |> Proof.global_terminal_proof methods; |
67 |> Proof.global_terminal_proof methods; |