equal
deleted
inserted
replaced
1087 |
1087 |
1088 (FIXME: read a name and show how to store theorems; see @{ML_ind note in LocalTheory}) |
1088 (FIXME: read a name and show how to store theorems; see @{ML_ind note in LocalTheory}) |
1089 |
1089 |
1090 *} |
1090 *} |
1091 |
1091 |
1092 ML_val{*val r = ref (NONE:(unit -> term) option)*} |
1092 ML_val{*val r = Unsynchronized.ref (NONE:(unit -> term) option)*} |
1093 ML{*let |
1093 ML{*let |
1094 fun after_qed thm_name thms lthy = |
1094 fun after_qed thm_name thms lthy = |
1095 LocalTheory.note Thm.theoremK (thm_name, (flat thms)) lthy |> snd |
1095 LocalTheory.note Thm.theoremK (thm_name, (flat thms)) lthy |> snd |
1096 |
1096 |
1097 fun setup_proof (thm_name, (txt, pos)) lthy = |
1097 fun setup_proof (thm_name, (txt, pos)) lthy = |