added Option_ord.thy

dropped local tsigs

some steps towards a refined treatment of equality

generic improvable syntax for targets

added hithero missing overloading.ML

tuned

whitespace tuning

clarified proposition

tuned proofs

canonical order on option type

added entries

check ISABELLE_BROWSER_INFO before cd;

replaced execute by system_out;

replaced execute by system_out;

added dummy version of string_of_pid;

use "ML-Systems/universal.ML"; specific system_out;

replaced execute by system_out;

proper dependency on ML-Systems/mosml.ML;

specific system_out (MosML lacks structure Posix); dummy implementation of Posix.ProcEnv.getpid;

* system/system_out provides a robust way to invoke external shell commands, with propagation of interrupts (after Poly/ML 5.2);

system_out: threaded version does not work for 5.1;

common setup for system_out/system;

added ML-Systems/system_shell.ML;

removed obsolete THIS_IS_ISABELLE_BUILD;

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;