581 text {* \blankline *} |
581 text {* \blankline *} |
582 |
582 |
583 ML {* Datatype_Data.get_info @{theory} @{type_name even_nat} *} |
583 ML {* Datatype_Data.get_info @{theory} @{type_name even_nat} *} |
584 |
584 |
585 text {* |
585 text {* |
586 For nested recursive datatypes, all types through which recursion takes place |
586 A few remarks concern nested recursive datatypes only: |
587 must be new-style datatypes. In principle, it should be possible to support |
587 |
588 old-style datatypes as well, but the command does not support this yet (and |
588 \begin{itemize} |
589 there is currently no way to register old-style datatypes as new-style |
589 \item The old-style, nested-as-mutual induction rule, iterator theorems, and |
590 datatypes). |
590 recursor theorems are generated under their usual names but with ``@{text |
591 |
591 "compat_"}'' prefixed (e.g., @{text compat_tree.induct}). |
592 An alternative is to use the old package's \keyw{rep\_datatype} command. The |
592 |
593 associated proof obligations must then be discharged manually. |
593 \item All types through which recursion takes place must be new-style datatypes |
|
594 or the function type. In principle, it should be possible to support old-style |
|
595 datatypes as well, but the command does not support this yet (and there is |
|
596 currently no way to register old-style datatypes as new-style datatypes). |
|
597 \end{itemize} |
|
598 |
|
599 An alternative to @{command datatype_new_compat} is to use the old package's |
|
600 \keyw{rep\_datatype} command. The associated proof obligations must then be |
|
601 discharged manually. |
594 *} |
602 *} |
595 |
603 |
596 |
604 |
597 subsection {* Generated Constants |
605 subsection {* Generated Constants |
598 \label{ssec:datatype-generated-constants} *} |
606 \label{ssec:datatype-generated-constants} *} |