src/Doc/ProgProve/Logic.thy
changeset 52220 73ddb9e6f6e8
parent 50630 e0e8b53534de
child 52562 0098bfe3be53
     1.1 --- a/src/Doc/ProgProve/Logic.thy	Tue Feb 12 12:22:44 2013 +0100
     1.2 +++ b/src/Doc/ProgProve/Logic.thy	Tue Feb 12 21:35:40 2013 +0100
     1.3 @@ -72,6 +72,7 @@
     1.4  \end{warn}
     1.5  
     1.6  \subsection{Sets}
     1.7 +\label{sec:Sets}
     1.8  
     1.9  Sets of elements of type @{typ 'a} have type @{typ"'a set"}.
    1.10  They can be finite or infinite. Sets come with the usual notation: