equal
deleted
inserted
replaced
38 kind prove_prop_parser |
38 kind prove_prop_parser |
39 end |
39 end |
40 *} |
40 *} |
41 |
41 |
42 ML {* |
42 ML {* |
43 val r = Unsynchronized.ref (NONE:(unit -> term) option) |
43 structure Result = Proof_Data( |
|
44 type T = unit -> term |
|
45 fun init thy () = error "Result") |
|
46 |
|
47 val result_cookie = (Result.get, Result.put, "Result.put") |
44 *} |
48 *} |
|
49 |
45 ML{* |
50 ML{* |
46 let |
51 let |
47 fun after_qed thm_name thms lthy = |
52 fun after_qed thm_name thms lthy = |
48 Local_Theory.note (thm_name, (flat thms)) lthy |> snd |
53 Local_Theory.note (thm_name, (flat thms)) lthy |> snd |
49 |
54 |
50 fun setup_proof (thm_name, (txt, pos)) lthy = |
55 fun setup_proof (thm_name, (txt, pos)) lthy = |
51 let |
56 let |
52 val trm = ML_Context.evaluate lthy true ("r", r) txt |
57 val trm = Code_Runtime.value lthy result_cookie ("", txt) |
53 in |
58 in |
54 Proof.theorem NONE (after_qed thm_name) [[(trm,[])]] lthy |
59 Proof.theorem NONE (after_qed thm_name) [[(trm,[])]] lthy |
55 end |
60 end |
56 |
61 |
57 val parser = Parse_Spec.opt_thm_name ":" -- Parse.ML_source |
62 val parser = Parse_Spec.opt_thm_name ":" -- Parse.ML_source |
61 Keyword.thy_goal (parser >> setup_proof) |
66 Keyword.thy_goal (parser >> setup_proof) |
62 end*} |
67 end*} |
63 |
68 |
64 |
69 |
65 |
70 |
|
71 |
66 end |
72 end |