removed unused add_substring; back to simple list implementation;

renamed syntax constant "_var" to "_variable", to avoid clash with internal token marker;

removed print mode "PGASCII" -- 7-bit ASCII communication now always enabled;

updated rendering of inner token markup;

more detailed inner token markup;

added numeral, which supercedes num, xnum, float; renamed xstr to inner_string;

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;