adapted Name.defaults_of;

removed obsolete xless; tuned zero_var_indexes;

clean: no special treatment of empty name; declare, invent: clean arguments;

removed obsolete xless;

replaced mk_listT by HOLogic.listT; trivial whitespace/comment changes

uniform treatment of num/xnum; read_xnum: proper handling of bin/hex;

replaced read_radixint by read_intinf;

removed str_to_int in favour of general Syntax.read_xnum;

num/xnum: bin or hex;

Name.internal; Name.invent_list;

tuned;

* Pure: structure Name;

Names of basic logical entities (variables etc.).

replaced Term.variant(list) by Name.variant(_list); removed obsolete mem_term;

Name.internal; Name.dest_skolem;

adapted to more efficient Name/Variable implementation; removed dead code;

replaced Term.variant(list) by Name.variant(_list); Name.internal;

maintain Name.context for fixes/defaults; more efficient inventing/renaming of local names (cf. name.ML);

removed obsolete mem_ix;

removed obsolete ins_ix, mem_ix, ins_term, mem_term; moved variant(list), invent_names, bound, dest_internal/skolem etc. to name.ML;

Name.dest_skolem;

Name.bound;

replaced Term.variant(list) by Name.variant(_list); Name.bound;

replaced Term.variant(list) by Name.variant(_list); Name.invent_list;

replaced Term.variant(list) by Name.variant(_list); Name.clean;

Name.invent_list;

added name.ML;

Name.is_bound;

removed obsolete mem_term;

Name.internal;

replaced Term.variant(list) by Name.variant(_list);

let_simproc: activate Variable.import;

Witness theorems of interpretations now transfered to current theory.

New function transfer_witness lifting Thm.transfer to witnesses.

hex and binary numerals (contributed by Rafal Kolanski)

minor optimization wrt. certifying terms

tuned;

tuned;

updated;

tuned interface; case_ss: proper context;

tuned interface;

removed dead code;

Element.prove_witness: context; Goal.prove_global;

prove_witness: context;

tuned exception handling;

prove/prove_multi: context; prove_global: theory + standard; tuned;

simprocs: no theory argument -- use simpset context instead; misc cleanup;

distinct simproc/simpset: proper context;

presburger_ss: proper context;

presburger_ss: proper context; Goal.prove: context;

tuned;

avoid Force_tac, which uses a different context;

Goal.prove: context;

tactic/method simpset: maintain proper context;

Goal.prove_global; SkipProof.prove: context;

Goal.prove_global;

simprocs: no theory argument -- use simpset context instead; tuned interfaces;

simprocs: no theory argument -- use simpset context instead;

updated;

updated Goal.prove, Goal.prove_global;