fixed problem with earlier commit about nominal_function_common; added facility for specifying an invariant - added a definition of frees_set which need a finiteness invariant
Function definitions- export proofs bout alpha_bn- equations like | "simp p (App t1 t2) = (if True then (App (simp p t1) (simp p t2)) else t1)" do not workParser 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 typeSmaller things:- maybe <type>_perm whould be called permute_<type>.simps; that would conform with the terminology in Nominal2Other:- nested recursion, like types "trm list" in a constructor- store information about defined nominal datatypes, so that it can be used to define new types that depend on these