| changeset 16417 | 9bc16273c2d4 |
| parent 16121 | a80aa66d2271 |
| child 17203 | 29b2563f5c11 |
| 16416:6061ae1f90f2 | 16417:9bc16273c2d4 |
|---|---|
5 |
5 |
6 header {* Program extraction for HOL *} |
6 header {* Program extraction for HOL *} |
7 |
7 |
8 theory Extraction |
8 theory Extraction |
9 imports Datatype |
9 imports Datatype |
10 files "Tools/rewrite_hol_proof.ML" |
10 uses "Tools/rewrite_hol_proof.ML" |
11 begin |
11 begin |
12 |
12 |
13 subsection {* Setup *} |
13 subsection {* Setup *} |
14 |
14 |
15 setup {* |
15 setup {* |