simplified Thm.instantiate and derivatives: the LHS refers to non-certified variables -- this merely serves as index into already certified structures (or is ignored);

clarified context;

clarified context;

Thm.cterm_of and Thm.ctyp_of operate on local context;

fixed some spelling mistakes

tuned signature;
tuned;

more standard fold/fold_rev;

misc tuning;

prefer existing beta_eta_conversion;

observe context more carefully when producing "fresh" variables -- for increased chances that method "subst" works in local context (including that of forked proofs);

eliminated some old material that is unused in the visible universe;

old term operations are legacy;

discontinued Name.variant to emphasize that this is old-style / indirect;

less pervasive names from structure Thm;

renamed varify/unvarify operations to varify_global/unvarify_global to emphasize that these only work in a global situation;

standardized filter/filter_out;

curried union as canonical list operation

dropped redundant gen_ prefix

replaced old_style infixes eq_set, subset, union, inter and variants by generic versions

Merge.

use long names for old-style fold combinators;

moved old add_type_XXX, add_term_XXX etc. to structure OldTerm;

moved old add_term_vars, add_term_frees etc. to structure OldTerm;

tuned headers -- adapted to usual conventions;

moved IsaPlanner from Provers to Tools;