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 bindingsSmaller things:- 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 datatypesBigger things:- nested recursion, like types "trm list" in a constructor- strong induction rules- check support equations for more bindings per constructor- automate the proofs that are currently proved with sorry: alpha_equivp- store information about defined nominal datatypes, so that it can be used to define new types that depend on these- make parser aware of bn functions that call other bn functions and reflect it in the datastructure passed to Fv/Alpha generation- make parser aware of recursive and of different versions of absLess 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