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).

Add get_succs

Add operations on preference tables (remove, set_default).

adjusted to new codegen_funcgr interface

added interface for plugging in preprocessors

additional auxiliary here

whitespace tuning

dropped dead code

shifted import order

dropped whitespace

changed name of interpretation linorder to order

proper simproc_setup; tuned ML setup;

added get_simproc, @{simproc};

added interface for target_naming;

added simproc_setup;

added def_simproc(_i) -- define named simprocs; tuned;

updated;

Now deals with simples cases where the input equations contain type variables See example in ReflectionEx.thy

refined algorithm

clarified code

exported interface for explicit error messages

added NestedEnvironment

Improved debugging

Streamlined and improved debugging messages

more fixes of arithmetic for min/max.