author | nipkow |
Tue, 12 Feb 2013 21:35:40 +0100 | |
changeset 52220 | 73ddb9e6f6e8 |
parent 52219 | 0a6d84c41dbf |
child 52221 | 3775bf0ea5b8 |
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: