# HG changeset patch # User Cezary Kaliszyk # Date 1271322354 -7200 # Node ID 0e70f3c82876a78352af68c3fa7bc89103a84738 # Parent 756982b4fe20bf62df17dacacc5020bc73cb33a1 Minor paper fixes. diff -r 756982b4fe20 -r 0e70f3c82876 Paper/Paper.thy --- a/Paper/Paper.thy Wed Apr 14 22:41:22 2010 +0200 +++ b/Paper/Paper.thy Thu Apr 15 11:05:54 2010 +0200 @@ -424,7 +424,7 @@ permutations. The sorts of atoms can be used to represent different kinds of variables, such as the term-, coercion- and type-variables in Core-Haskell. It is assumed that there is an infinite supply of atoms for each - sort. However, in the intrest of brevity, we shall restrict ourselves + sort. However, in the interest of brevity, we shall restrict ourselves in what follows to only one sort of atoms. Permutations are bijective functions from atoms to atoms that are @@ -1032,7 +1032,7 @@ As will shortly become clear, we cannot return an atom in a binding function that is also bound in the corresponding term-constructor. That means in the - example above that the term-constructors @{text PVar} and @{text PTup} must not have a + example above that the term-constructors @{text PVar} and @{text PTup} may not have a binding clause. In the version of Nominal Isabelle described here, we also adopted the restriction from the Ott-tool that binding functions can only return: the empty set or empty list (as in case @{text PNil}), a singleton set or singleton @@ -2019,7 +2019,7 @@ definitions to equivariant functions (for such functions it is possible to provide more automation). - There are some restrictions we imposed in this paper, we like to lift in + There are some restrictions we imposed in this paper, that we would like to lift in future work. One is the exclusion of nested datatype definitions. Nested datatype definitions allow one to specify, for instance, the function kinds in Core-Haskell as @{text "TFun string (ty list)"} instead of the unfolded