| changeset 46165 | 3c5d3d286055 |
| parent 45916 | c478d1876371 |
| child 46471 | 1bbbac9a0cb0 |
| 46164:57def0b39696 | 46165:3c5d3d286055 |
|---|---|
306 |
306 |
307 text {* @{text "DERIV_intros"} *} |
307 text {* @{text "DERIV_intros"} *} |
308 ML {* |
308 ML {* |
309 structure Deriv_Intros = Named_Thms |
309 structure Deriv_Intros = Named_Thms |
310 ( |
310 ( |
311 val name = "DERIV_intros" |
311 val name = @{binding DERIV_intros} |
312 val description = "DERIV introduction rules" |
312 val description = "DERIV introduction rules" |
313 ) |
313 ) |
314 *} |
314 *} |
315 |
315 |
316 setup Deriv_Intros.setup |
316 setup Deriv_Intros.setup |