renamed token markup "_xstr" to "_inner_string";

removed dead code; proper "_numeral" token markup; proper printing of arguments (higher-order numerals);

renamed ThyEdit (in thy_edit.ML) to ThySyntax (in thy_syntax.ML);

tuned;

Isar.command: plain Position.id; tuned;

added type 'a parser, simplified signature;

added type 'a parser, simplified signature; added internal_command wrapper; tuned;

added type 'a parser, simplified signature; moved properties to value_parse.ML; moved props_text to isar_syn.ML;

added props_text (from outer_parse.ML);

added Isar/value_parse.ML: Outer syntax parsers for basic ML values.

added id; tuned;

MetaSimplifier.SIMPLIFIER;

fixed assumption proof;

tuned header and description of boot files;

merged;

normalized some ML type/val aliases;

assumption/close: discontinued implicit prems;

avoid implicit use of prems;

updated generated files;

eliminated implicit use of prems; unified fact names: a, b, ab;

updated generated files;

updated type 'a lazy; proper name for type simpset;

proper import of ~~/src/HOL/ex/ReflectedFerrack;

crude adaption to intermediate class/locale version;

crude adaption to new locales;

avoid implicit prems -- tuned proofs;

avoid implicit use of prems;

Term.add_consts;

eliminated OldTerm.(add_)term_consts; eliminated polymorphic version of insert;

avoid polymorphic equality;

eliminated OldTerm.(add_)term_consts;

added canonical add_const_names, add_consts;

provide structure CharVector;

isabelle-process; provide structure Word; provide IntInf.log2;

updated sessions;

removed unused add_term_free_names;

eliminated OldTerm.add_term_free_names;

updated header;

Term.declare_typ_names, Term.declare_term_frees;

added declare_term_frees; tuned signature;

Term.declare_term_frees;

qualified Term.rename_wrt_term;

moved old add_type_XXX, add_term_XXX etc. to structure OldTerm; use regular Term.add_XXX etc.;

use fold_aterms directly;

use exists_Const directly;

use regular Term.add_XXX etc.;

moved old add_type_XXX, add_term_XXX etc. to structure OldTerm; use exists_Const directly;

moved old add_type_XXX, add_term_XXX etc. to structure OldTerm;

moved term order operations to structure TermOrd (cf. Pure/term_ord.ML); tuned signature of structure Term;

use exists_subterm directly; moved old add_term_vars, add_term_frees etc. to structure OldTerm;

use exists_subterm directly;

use regular Term.add_vars, Term.add_frees etc.; moved old add_term_vars, add_term_frees etc. to structure OldTerm;

moved old add_term_vars, add_term_frees etc. to structure OldTerm;

use regular Term.add_vars, Term.add_frees etc.;

added old_term.ML;

Some old-style term operations.

freeze_thaw: canonical Term.add_XXX operations; varify: regular name context;

varify: regular name context;

canonical Term.add_var_names, Term.add_tvar_namesT;

canonical Term.add_var_names;