moved the infrastructure from the nominal_tags file to nominal_thmdecls file, and adapted the code to conform with informal Isabelle programming conventions

Exporting curried versions of tail recursive equations instead of internal ones

proper use of NameSpace.is_qualified (avoids compatibility issues of the SML B library);

removed non-modular comment;

interpretation: attempt to be more serious about name_morphism;

added full_naming;

tuned oracle interface; simproc_setup: added identifier;

added print_strings;

old-fashioned abstype ctyp/cterm/thm prevents accidental equality tests;

def_simproc(_i): tuned interface; tuned simprocs environment;

added cterm interface;

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;

proper use of PureThy.has_name_hint instead of hard-wired string'';

removed non-modular comment;

new theorem int_infinite

Fix tell_thm_deps to match changse in PureThy.

Expose hard-wired string which was changed and broke Proof General.

clarified error message

clarified command annotation

changed cong alist - now using AList operations instead of overwrite_warn

dropped Output.update_warn

print translation for record types with empty-sorted type variables raise Match instead of producing an error

dropped lemma duplicates in HOL.thy

Tidying; more debugging information. New reference unwanted_types.

Tweak preferences for PGIP interfaces. Make <askids> return theory successors instead of parents (ideally should be content elements).