made some small changes to generate nicer latex-output

split the files - Iteration.thy contains the big proof of the iteration combinator - Recursion.thy derives from Iteration the recursion combinator - lam_substs.thy contains the examples (size, substitution and parallel substitution)

Added in a signature.

fixed a problem where a permutation is not analysed when the term is of the form (pi o f) x1...xn This was the case because the head of this term is the constant "nominal.perm". Now an applicability predicate decides the right behaviour of the simproc

streamlined the proof

refined representation of codegen intermediate language

some small tunings