--- a/Pearl/Paper.thy	Thu Apr 08 00:25:08 2010 -0700
+++ b/Pearl/Paper.thy	Thu Apr 08 00:47:13 2010 -0700
@@ -1148,9 +1148,9 @@
   user just needs to specify \isacommand{atom\_decl}~~@{text "var (ty)"}
   where the argument, or arguments, are datatypes for which we can automatically
   define an injective function like @{text "sort_ty"} (see \eqref{sortty}).
-  Our hope is that with this approach Benzmueller and Paulson, the authors of 
-  \cite{PaulsonBenzmueller}, can make headway with formalising their results 
-  about simple type theory.  
+  Our hope is that with this approach Benzmueller and Paulson can make
+  headway with formalising their results
+  about simple type theory \cite{PaulsonBenzmueller}.
   Because of its limitations, they did not attempt this with the old version 
   of Nominal Isabelle. We also hope we can make progress with formalisations of
   HOL-based languages.
@@ -1195,7 +1195,7 @@
   zero to return zero.
 
   We noticed only one disadvantage of the permutations-as-functions: Over
-  lists we can easily perform inductions. For permutation made up from
+  lists we can easily perform inductions. For permutations made up from
   functions, we have to manually derive an appropriate induction principle. We
   can establish such a principle, but we have no real experience yet whether ours
   is the most useful principle: such an induction principle was not needed in