Automatically created functions:

  ty1_tyn.bn[simp]        lifted equations for bn funs

  ty1_tyn.fv[simp]        lifted equations for fv funs

  ty1_tyn.perm[simp]      lifted permutation equations

  ty1_tyn.distinct[simp]  lifted distincts

  ty1_tyn.eq_iff

  ty1_tyn.induct

  ty1_tyn.inducts

  instance ty1 and tyn :: fs

  ty1_tyn.supp            empty when for too many bindings

Parser should check that:

- types of bindings match types of binding functions

- fsets are not bound in lst bindings

- bound arguments are not datatypes

- binder is referred to by name and not by type

Smaller things:

- lam.perm should be called permute_lam.simps (that is 

  the convention from Nominal2)

- maybe <type>_perm whould be called permute_<type>.simps;

  that would conform with the terminology in Nominal2

- we also need to lift the size function for nominal

  datatypes

- Abs.thy contains lemmas for equivariance of the alphas;

  they are not yet used anywhere

Bigger things:

- Parser adds syntax for raw datatype, but should

  add for lifted datatype.

- the alpha equivalence for

   Let as::assn t::trm   bind "bn as" in t

  creates as premise

    EX pi. as ~~bn as' /\ (bn as, t) ~~lst (bn as', t')

  but I think it should be

    as ~~bn as' /\ EX pi. (bn as, t) ~~lst (bn as', t')    

  (both are equivalent, but the second seems to be closer to

   the fv-function)

- when there are more than one shallow binder, then alpha

  equivalence creates more than one permutation. According

  to the paper, this is incorrect.

  Example in Classical.thy.

- check whether weirdo example in TestMorePerm works

  with shallow binders

- nested recursion, like types "trm list" in a constructor

- define permute_bn automatically and prove properties of it

- prove renaming-of-binders lemmas

- strong induction rules

- check support equations for more bindings per constructor

- For binding functions that call other binding functions

  the following are proved with cheat_tac: constr_rsp

- store information about defined nominal datatypes, so that

  it can be used to define new types that depend on these

- make parser aware of recursive and of different versions of abs

Less important:

- fv_rsp uses 'blast' to show goals of the type:

  a u b = c u d   ==>  a u x u b = c u x u d

When cleaning:

- remove all 'PolyML.makestring'.