| changeset 48236 | e174ecc4f5a4 |
| parent 48235 | 40655464a93b |
| child 48239 | 0016290f904c |
| 48235:40655464a93b | 48236:e174ecc4f5a4 |
|---|---|
6 |
6 |
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 |
|
12 declare [[sledgehammer_instantiate_inducts]] |
|
11 |
13 |
12 ML {* |
14 ML {* |
13 open MaSh_Import |
15 open MaSh_Import |
14 *} |
16 *} |
15 |
17 |