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: