new-style definitions/abbreviations;

added ex/Abstract_NAT.thy;

tuned;

tuned;

removed silly stuff

* Isar/locales: new derived specification elements 'definition', 'abbreviation', 'axiomatization';

added abbreviation(_i);

added put_thms_internal: local_naming, no fact index; tuned;

added put_thms_internal; tuned;

added abbrev element;

added 'abbreviation'; tuned;

added premsN;

Proof.put_thms_internal;

removed pointless replace;

tuned;

dest_def: actually return beta-eta contracted equation;

derived specifications: definition, abbreviation, axiomatization;

updated;

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;