equal
deleted
inserted
replaced
596 |
596 |
597 datatype_compat even_nat odd_nat |
597 datatype_compat even_nat odd_nat |
598 |
598 |
599 text {* \blankline *} |
599 text {* \blankline *} |
600 |
600 |
601 ML {* Datatype_Data.get_info @{theory} @{type_name even_nat} *} |
601 ML {* Old_Datatype_Data.get_info @{theory} @{type_name even_nat} *} |
602 |
602 |
603 text {* |
603 text {* |
604 The syntactic entity \synt{name} denotes an identifier \cite{isabelle-isar-ref}. |
604 The syntactic entity \synt{name} denotes an identifier \cite{isabelle-isar-ref}. |
605 |
605 |
606 The command is interesting because the old datatype package provides some |
606 The command is interesting because the old datatype package provides some |