type simproc: explicitl dependency of morphism; added eq_simproc, morph_simproc; renamed mk_simproc' to make_simproc -- primary interface;

load morphism.ML later;

added the two renaming functions from my PhD

added an infrastructure that allows the user to declare lemmas to be equivariance lemmas; the intention is to use these lemmas in automated tools but also can be employed by the user

a few additions and deletions

tuned;