diff -r 86122d793f32 -r 0c958e385691 Pearl/document/root.tex --- 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