# HG changeset patch
# User Brian Huffman <brianh@cs.pdx.edu>
# Date 1270712948 25200
# Node ID 7a99da5975e649f5cbd84381e5a2c709feebea0a
# Parent  22e6571d0bb2a9b3c9832dbcf949a8861150b6f8# Parent  3764ed518ee580728af27ef1c58f7650c132affb
merged

diff -r 3764ed518ee5 -r 7a99da5975e6 Pearl/Paper.thy
--- a/Pearl/Paper.thy	Thu Apr 08 09:13:36 2010 +0200
+++ b/Pearl/Paper.thy	Thu Apr 08 00:49:08 2010 -0700
@@ -741,7 +741,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}
@@ -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