cache improvements

variable counter is now also cached

adapted to kernel changes

tuned subst_bound(s);

fixed bugs, added caching

added cases_node; replaced body_context_of by body_context_node, removed no_body_context; copy: ProofContext.transfer; added present_local_theory, present_proof; removed internal command interface;

replaced qualified_force_prefix to sticky_prefix; do not export read_terms;

removed distinct, renamed gen_distinct to distinct; replaced qualified_force_prefix by qualified_names/sticky_prefix;

check_text: Toplevel.node option;

init/exit no longer change the theory (no naming); added naming, restore_naming, mapping;

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