| author | blanchet |
| Mon, 01 Sep 2014 16:17:47 +0200 | |
| changeset 58121 | d7550665da31 |
| parent 58120 | a14b8d77b15a |
| child 58122 | eaac3e01158a |
--- a/src/Doc/Datatypes/Datatypes.thy Mon Sep 01 16:17:47 2014 +0200 +++ b/src/Doc/Datatypes/Datatypes.thy Mon Sep 01 16:17:47 2014 +0200 @@ -598,7 +598,7 @@ text {* \blankline *} - ML {* Datatype_Data.get_info @{theory} @{type_name even_nat} *} + ML {* Old_Datatype_Data.get_info @{theory} @{type_name even_nat} *} text {* The syntactic entity \synt{name} denotes an identifier \cite{isabelle-isar-ref}.