| changeset 2048 | 20be95dce643 |
| parent 2047 | 31ba33a199c7 |
| child 2076 | 6cb1a4639521 |
| 2047:31ba33a199c7 | 2048:20be95dce643 |
|---|---|
352 |
352 |
353 ML {* |
353 ML {* |
354 (* for testing porposes - to exit the procedure early *) |
354 (* for testing porposes - to exit the procedure early *) |
355 exception TEST of Proof.context |
355 exception TEST of Proof.context |
356 |
356 |
357 val STEPS = 3 |
357 val STEPS = 10 |
358 *} |
358 *} |
359 |
359 |
360 ML {* |
360 ML {* |
361 fun nominal_datatype2 dts bn_funs bn_eqs bclauses lthy = |
361 fun nominal_datatype2 dts bn_funs bn_eqs bclauses lthy = |
362 let |
362 let |