Extra parameter for new_type command in nomdatatype allowing for multi-types.

Doesn't work unless each 'type' allows a 'VAR' constructor, which is not the case
in first order formulas and terms, for example.

General code for automatically proving type-bijection results in src/1.

This code was already used in the prototypical nominal datatype
package code; now it's more generally available. The code implements
one big function (for the moment) that proves all the nice results
(various rewrite rules) that are immediate consequences of the usual
type bijection theorem. In addition, the function defines the abs-rep
constants with stereotyped names.

Extract a usable half-way point from nominal_datatype branch.

This replaces the is_perm predicate with a type embodying that predicate.
It doesn't include the subsequent work on allowing multiple 'atom' types.

Terms and labelled terms now derived from generic terms.

This is a big change that points to the implementation of a complete
nominal datatype package. The use of generic terms means that we only
need to do one hairy quotient, and one hairy derivation of a recursion
principle.

The recursion principle in question features a new "FCB" (one of the
side-conditions that need to be proved in order to get a recursive
function admitted). Though I think it's better, it can be a little
fiddlier to prove. It's also stronger, so in theory, there may be
reasonable functions that the new FCB rejects. It should certainly be
possible to automate the bulk of the new fiddly proofs.