changeset 1859 | 900ef226973e |
parent 1847 | 0e70f3c82876 |
child 1890 | 23e3dc4f2c59 |
--- a/Paper/Paper.thy Thu Apr 15 15:56:38 2010 +0200 +++ b/Paper/Paper.thy Thu Apr 15 16:01:28 2010 +0200 @@ -774,7 +774,7 @@ \end{center} \noindent - indicating that a set (or list) @{text as} is abstracted in @{text x}. We will + indicating that a set (or list) of atoms @{text as} is abstracted in @{text x}. We will call the types \emph{abstraction types} and their elements \emph{abstractions}. The important property we need to derive is the support of abstractions, namely: