| changeset 48235 | 40655464a93b |
| parent 48234 | 06216c789ac9 |
| child 48236 | e174ecc4f5a4 |
| 48234:06216c789ac9 | 48235:40655464a93b |
|---|---|
7 theory MaSh_Import |
7 theory MaSh_Import |
8 imports MaSh_Export |
8 imports MaSh_Export |
9 uses "mash_import.ML" |
9 uses "mash_import.ML" |
10 begin |
10 begin |
11 |
11 |
12 ML {* |
|
13 open MaSh_Import |
|
14 *} |
|
15 |
|
16 ML {* |
|
17 val do_it = true (* switch to "true" to generate the files *); |
|
18 val thy = @{theory List} |
|
19 *} |
|
20 |
|
21 ML {* |
|
22 if do_it then import_and_evaluate_mash_suggestions @{context} thy "/tmp/mash_suggestions2" |
|
23 else () |
|
24 *} |
|
25 |
|
12 end |
26 end |