| changeset 54118 | f5fc8525838f |
| parent 53120 | 43d5f3d6d04e |
| child 54717 | 42c209a6c225 |
| 54117:32730ba3ab85 | 54118:f5fc8525838f |
|---|---|
61 () |
61 () |
62 *} |
62 *} |
63 |
63 |
64 ML {* |
64 ML {* |
65 if do_it then |
65 if do_it then |
66 generate_isar_dependencies @{context} thys linearize |
66 generate_isar_dependencies @{context} range thys linearize |
67 (prefix ^ "mash_dependencies") |
67 (prefix ^ "mash_dependencies") |
68 else |
68 else |
69 () |
69 () |
70 *} |
70 *} |
71 |
71 |