# HG changeset patch
# User nipkow
# Date 1360701340 -3600
# Node ID 73ddb9e6f6e8c17c06d045baa736fc055aef91dd
# Parent  0a6d84c41dbf7272be76f88ba6df1fd6b4888573
tuned

diff -r 0a6d84c41dbf -r 73ddb9e6f6e8 src/Doc/ProgProve/Logic.thy
--- a/src/Doc/ProgProve/Logic.thy	Tue Feb 12 12:22:44 2013 +0100
+++ b/src/Doc/ProgProve/Logic.thy	Tue Feb 12 21:35:40 2013 +0100
@@ -72,6 +72,7 @@
 \end{warn}
 
 \subsection{Sets}
+\label{sec:Sets}
 
 Sets of elements of type @{typ 'a} have type @{typ"'a set"}.
 They can be finite or infinite. Sets come with the usual notation: