| changeset 328 | c0cae24b9d46 |
| parent 324 | 4172c0743cf2 |
| child 394 | 0019ebf76e10 |
| 327:ce754ad78bc9 | 328:c0cae24b9d46 |
|---|---|
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 = ref (NONE:(unit -> term) option) |
43 val r = Unsynchronized.ref (NONE:(unit -> term) option) |
44 *} |
44 *} |
45 ML{* |
45 ML{* |
46 let |
46 let |
47 fun after_qed thm_name thms lthy = |
47 fun after_qed thm_name thms lthy = |
48 LocalTheory.note Thm.theoremK (thm_name, (flat thms)) lthy |> snd |
48 LocalTheory.note Thm.theoremK (thm_name, (flat thms)) lthy |> snd |