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