Review “injective functions” paper↔algorithm equivalence proof

[clange]

Now that @caminati has committed a paper↔algorithm equivalence proof for “all injective functions from one set to another” in b.thy, I should review, reorganise, simplify and document it. And then, once more, announce it to Isabelle (as in #3).

@caminati noted about the relevance to Isabelle:

The formalization work spawned new relevant definitions: when a relation is a function, in a set-theoretical sense (runiq), the inverse operator, the pasting operator. Most importantly, it spawned a lot of basic results about those; which, apart from coding style, I feel make a useful addition to the Relation.thy already present in the standard library.

[clange]

Reviewing, reorganising, simplifying and documenting have been done some time around September 2013.

I've rolled out "announcing" to #42.