equal
deleted
inserted
replaced
3 Author: Stefan Berghofer, TU Muenchen |
3 Author: Stefan Berghofer, TU Muenchen |
4 *) |
4 *) |
5 |
5 |
6 header {* Program extraction for HOL *} |
6 header {* Program extraction for HOL *} |
7 |
7 |
8 theory Extraction = Datatype |
8 theory Extraction |
9 files |
9 import Datatype |
10 "Tools/rewrite_hol_proof.ML": |
10 files "Tools/rewrite_hol_proof.ML" |
|
11 begin |
11 |
12 |
12 subsection {* Setup *} |
13 subsection {* Setup *} |
13 |
14 |
14 ML_setup {* |
15 ML_setup {* |
15 fun realizes_set_proc (Const ("realizes", Type ("fun", [Type ("Null", []), _])) $ r $ |
16 fun realizes_set_proc (Const ("realizes", Type ("fun", [Type ("Null", []), _])) $ r $ |