tuning
authorblanchet
Tue, 29 Mar 2016 09:49:39 +0200
changeset 62740 69e4a4fffea9
parent 62739 628c97d39627
child 62741 1ddfe28117e9
tuning
src/Doc/Datatypes/Datatypes.thy
--- a/src/Doc/Datatypes/Datatypes.thy	Tue Mar 29 09:45:54 2016 +0200
+++ b/src/Doc/Datatypes/Datatypes.thy	Tue Mar 29 09:49:39 2016 +0200
@@ -460,7 +460,7 @@
   \label{ssec:datatype-command-syntax}\<close>
 
 subsubsection \<open>\keyw{datatype}
-  \label{sssec:datatype-new}\<close>
+  \label{sssec:datatype}\<close>
 
 text \<open>
 \begin{matharray}{rcl}
@@ -1569,7 +1569,7 @@
   \label{ssec:primrec-command-syntax}\<close>
 
 subsubsection \<open>\keyw{primrec}
-  \label{sssec:primrec-new}\<close>
+  \label{sssec:primrec}\<close>
 
 text \<open>
 \begin{matharray}{rcl}