--- a/Pearl/document/root.tex	Tue Apr 06 07:36:15 2010 +0200
+++ b/Pearl/document/root.tex	Tue Apr 06 14:08:06 2010 +0200
@@ -1,4 +1,4 @@
-\documentclass[runningheads]{llncs}
+\documentclass{llncs}
 \usepackage{times}
 \usepackage{isabelle}
 \usepackage{isabellesym}
@@ -38,7 +38,7 @@
 lists of pairs of atoms, we now use a more abstract representation based on
 functions.  Second, whereas the earlier work modeled different sorts of atoms
 using different types, we now introduce a unified atom type that includes all
-sorts of atoms. Interestingly, we allow swappings, that is permutations build up by
+sorts of atoms. Interestingly, we allow swappings, that is permutations build from
 two atoms, to be ill-sorted.  As a result of these design changes, we can iron
 out inconveniences for the user, considerably simplify proofs and also
 drastically reduce the amount of custom ML-code. Furthermore we can extend the