token translations: context dependent, result Pretty.T;

Pretty.mark;

unused_thms: sort_distinct;

Sign.add_path;

removed obsolete BASIC_THM_DEPS; unused_thms: simplified signature, use proper PureThy.facts_of; misc tuning;

pretty_theorems: use proper PureThy.facts_of;

Facts.extern_static;

PureThy.defined_fact; unused_thms: simplified signature;

renamed check_fact to defined_fact;

removed unused space_of; added defined, fold_static; renamed dest_table to dest_static; renamed extern_table to extern_static;

valid_facts: more elementary version using Facts.fold_static;

Facts.dest_static;

Auxiliary permutation functions are no longer declared using add_consts_i, because add_primrec_overloaded can do this as well.

removed unused TLA/Memory/MIParameters.thy;

removed obsolete valid_thms; removed obsolete premsN binding; PureThy.get_fact: pass dynamic context;

removed obsolete premsN;

PureThy.get_fact: pass dynamic context;

tuned;

removed obsolete get_fact_silent; PureThy.get_fact: pass dynamic context; tuned;

tuned proofs;

Added entry for unused_thms command.

Adapted to new primrec package.

Added add_primrec_global and add_primrec_overloaded functions (thanks to Markus).

educated guess for infix syntax

removed test artefacts

proof endings: no Toplevel.print!

all_valid_thms: use new facts tables;

Theory.subthy;

Facts.intern, Facts.extern_table;

IsarCmd.hide_names;