standard congs;

Now rename_params_rule merely issues warnings--and does nothing--if the renaming cannot be performed. Previously it raised a fatal error.

Now Datatype.occs_in_prems prints the necessary warning ITSELF. It is also easier to invoke and even works if the induction variable is a parameter (rather than a free variable).

Uses new version of Datatype.occs_in_prems

auto update

Removal of tactical STATE

fixed polymorphic val;

tuned congs: standard;

improved simp tracing;

added simplification meta rules;