evaluate antiquotes depending on Toplevel.node option;

simplified presentation commands;

sane version of distinct_subgoals_tac, based on composition with Drule.distinct_prems_rl;

removed qualified_force_prefix; added sticky_prefix;

replaced qualified_force_prefix to sticky_prefix;

chop is no longer pervasive; removed obsolete thms_containing;

rewrite_cterm: Thm.adjust_maxidx prevents unnecessary increments on rules;

added distinct_prems_rl;

specifications_of: avoid partiality;

counter example: avoid vacuous trace;

cannot use section before setup;

used Tactic.distinct_subgoals_tac;

removed distinct, renamed gen_distinct to distinct;

added lemma pt_perm_compose'

got rid of superfluous linorder_neqE-instance for int.

typo in a comment fixed

exported some interfaces useful for other code generator approaches

some fixes

exported specifications_of

added theory of executable rational numbers

improved handling of iml abstractions

fixed tracing

Adapted to Context.generic syntax.

Fixed a bug of type unification.

* ML/Pure/General: improved join interface for tables;

consts: maintain thy version for efficient transfer; ins_sorts: Vartab.replace is slower than Vartab.update, but might avoid some copying of table structure;

tuned;

export exception SAME (for join); join: use internal modify, no option type (handle SAME/DUP instead); defined: simplified copy of lookup code, avoids allocation of option constructor; added replace, which does not change equal entries;

low-level tuning of merge: maintain identity of accesses; simplified TableFun.join;

share exception UNDEF with Table; simplified TableFun.join;