| changeset 183 | 6acf9e001038 |
| parent 83 | e8f352546ad8 |
| child 319 | 0ae9d9e66cb7 |
| 182:c7eff9882bd8 | 183:6acf9e001038 |
|---|---|
1 theory Prove |
1 theory Prove |
2 imports Main |
2 imports Main |
3 begin |
3 begin |
4 |
4 |
5 ML {* |
5 ML {* |
6 val r = ref (NONE:(unit -> term) option) |
6 val r = Unsynchronized.ref (NONE:(unit -> term) option) |
7 *} |
7 *} |
8 |
8 |
9 ML {* |
9 ML {* |
10 let |
10 let |
11 fun after_qed thm_name thms lthy = |
11 fun after_qed thm_name thms lthy = |