# HG changeset patch
# User kleing
# Date 1363775536 -3600
# Node ID c5c466706549bc796c7885120d148e78dc34054b
# Parent  6cd801fabb34bf5934fa0e115830c52aec726621
add label for referencing in semantics book

diff -r 6cd801fabb34 -r c5c466706549 src/Doc/ProgProve/Types_and_funs.thy
--- a/src/Doc/ProgProve/Types_and_funs.thy	Wed Mar 20 11:16:31 2013 +0100
+++ b/src/Doc/ProgProve/Types_and_funs.thy	Wed Mar 20 11:32:16 2013 +0100
@@ -16,6 +16,7 @@
 Type synonyms are expanded after parsing and are not present in internal representation and output. They are mere conveniences for the reader.
 
 \subsection{Datatypes}
+\label{sec:datatypes}
 
 The general form of a datatype definition looks like this:
 \begin{quote}