added 'value'; tuned;

- put declarations inside a structure (NominalPermeq) - dynamic_thm(s) now looks up theorems in theory associated with proof state (rather than in context associated with simpset) - finite_guess_tac now automatically adds some extra rules about supp to the simpset

- nominal_permeq.ML is now loaded before nominal_package.ML - methods and tactics in nominal_permeq.ML are now defined inside structure NominalPermeq, therefore the names in the method_setup section had to be changed

Implemented proofs of equivariance and finite support for graph of recursion combinator.

Method intro_locales replaced by intro_locales and unfold_locales.

updated