obsolete (cf. ML-Systems/polyml_common.ML);

renamed polyml-old-basis.ML to polyml_old_basis.ML;

rearrangements to make latest Poly/ML the default, not old 4.x;

cleaned-up ML-Systems;

tuned comment;

removed obsolete THIS_IS_ISABELLE_BUILD feature; moved external provers further up; no HOL4_PROOFS by default;

removed obsolete THIS_IS_ISABELLE_BUILD feature: change environment after getsettings (works due to static scoping);

removed obsolete THIS_IS_ISABELLE_BUILD feature;

removed obsolete THIS_IS_ISABELLE_BUILD/MAKEBIN feature;

renamed test_markup to output_markup; added full_markup mode, with token translations;

IsabelleProcess.output_markup;

closeup: minor tuning of term traversal;

ISABELLE_LINE_EDITOR: prefer rlwrap, which passes interrupts properly;

explicit referencing of background facts;

explicit referencing of background facts;

explicit referencing of background facts;

indexing literal facts: exclude background context;

put_thms: do not index facts here (affects prems/this/calculation in particular);

explicit referencing of background facts;

HOL/Library/RBT.thy;

NEWS: RBTs, renamings in ZF

Use conversions instead of simplifier. tuned

added new example

tuned

continued localization

new theory of red-black trees, an efficient implementation of finite maps.

Generalized Zorn and added well-ordering theorem

tuned ML code, more antiquotations;

misc cleanup of embedded ML code; use more antiquotations; tuned;

added @{const} antiquotation;

use more antiquotations;

unused_thms: print via official context (ProofContext.pretty_fact), not just the theory certificate (Display.pretty_thm); tuned;