# HG changeset patch # User wenzelm # Date 1514921921 -3600 # Node ID 79260409a6804190be37054cbda31ef27eb8eef1 # Parent 4c94ec0488c7335e683396a0e579e3cff3ede11f old_datatype no longer exists (cf. 706b1cf7b76d); diff -r 4c94ec0488c7 -r 79260409a680 src/Doc/Datatypes/Datatypes.thy --- a/src/Doc/Datatypes/Datatypes.thy Tue Jan 02 19:52:36 2018 +0100 +++ b/src/Doc/Datatypes/Datatypes.thy Tue Jan 02 20:38:41 2018 +0100 @@ -1217,6 +1217,7 @@ @{text "[of \]"} syntax. \end{itemize} +%FIXME old_datatype no longer exists The old command is still available as \keyw{old_datatype} in theory \<^file>\~~/src/HOL/Library/Old_Datatype.thy\. However, there is no general way to register old-style datatypes as new-style datatypes. If the objective diff -r 4c94ec0488c7 -r 79260409a680 src/Doc/Isar_Ref/HOL_Specific.thy --- a/src/Doc/Isar_Ref/HOL_Specific.thy Tue Jan 02 19:52:36 2018 +0100 +++ b/src/Doc/Isar_Ref/HOL_Specific.thy Tue Jan 02 20:38:41 2018 +0100 @@ -712,13 +712,10 @@ text \ \begin{matharray}{rcl} - @{command_def (HOL) "old_datatype"} & : & \theory \ theory\ \\ @{command_def (HOL) "old_rep_datatype"} & : & \theory \ proof(prove)\ \\ \end{matharray} @{rail \ - @@{command (HOL) old_datatype} (spec + @'and') - ; @@{command (HOL) old_rep_datatype} ('(' (@{syntax name} +) ')')? (@{syntax term} +) ; @@ -727,9 +724,6 @@ cons: @{syntax name} (@{syntax type} * ) @{syntax mixfix}? \} - \<^descr> @{command (HOL) "old_datatype"} defines old-style inductive - datatypes in HOL. - \<^descr> @{command (HOL) "old_rep_datatype"} represents existing types as old-style datatypes.