--- a/Pearl/Paper.thy	Thu Apr 08 10:25:13 2010 +0200
+++ b/Pearl/Paper.thy	Thu Apr 08 10:25:38 2010 +0200
@@ -740,7 +740,7 @@
   provided @{thm (prem 1) finite_supp_unique[no_vars]},
   @{thm (prem 2) finite_supp_unique[no_vars]}, and for
   all @{text "a \<in> S"} and all @{text "b \<notin> S"}, with @{text a}
-  and @{text b} having the same sort, then \mbox{@{term "(a \<rightleftharpoons> b) \<bullet> x \<noteq> x"}}
+  and @{text b} having the same sort, \mbox{@{term "(a \<rightleftharpoons> b) \<bullet> x \<noteq> x"}}
   \end{lemma}
 
   \begin{proof}
@@ -1147,9 +1147,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.
@@ -1194,7 +1194,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