added interface for command-line option;

removed obsolete prompt and channel markups; replaced prompt markup by prompt channel setup (avoids left-over XML encoding); tuned;

replaced prompt markup by prompt channel setup;

removed obsolete prompt markup;

removed unused of_stream; tty: Output.prompt, avoid low-level TextIO;

added explicit prompt channel (prompt_fn/prompt); tuned;

removed obsolete prompt and channel markups;

Tuned relevant premises selection

tuned comments;

added symbol output mode, with XML escapes; improved message markup: get first position from body text; added INIT message, with pid and session property; removed adhoc PID handling; tuned;

export session id;

secure_main: removed separate welcome;

removed unused text_charref, cdata; added plain_content;

added INIT message, with pid and session property; removed adhoc PID handling;

more instantiation

adhering to instantiation policy

cleaned up some proofs

simplified some proofs

partially adapted to new inversion rules

adapted to new inversion rules

fixed typo

improved warning

add new is_ub lemmas; clean up directed_finite proofs

new instance proofs for classes finite_po, chfin, flat

new lemma flat_less_iff

generalized chfindom_monofun2cont

Implemented proof of strong case analysis rule.

Added function fresh_const.

Added function partition_rules'.

another attempt to disable documents;

simplified position_props, always include line/file fields;

replaced thread_properties by simplified version in position.ML;

nested_command: simplified properties vs. position -- the latter also includes id now;

type T: based on properties, added id field; added thread_data, setmp_thread_data (formerly in toplevel.ML); tuned signature;

moved id to position properties;

instance unit :: finite_po

new axclass finite_po < finite, po

add lub_maximal lemmas; modify conclusion of directed_finiteD; declare not_directed_empty [simp]

added class Property: basic Isabelle properties;

tuned relevance test for presburger

output message properties: id or position;

toplevel print_exn: proper setmp_thread_properties;

added id property;

Result: added props field; tuned;

remove legacy ML bindings

new-style theorem references

fix theorem references

generalized and simplified proof of adm_Finite

new lemma adm_upward

Tuned (type information in Lemmas)

Changed order of tactics in presburger --- thinning before case splits

maintain thread transition properties;

setmp_thread_data;

added setmp_thread_data;

type transition: added properties field;

added properties;

Isabelle.command: IsarCmd.nested_command (with properties);

added nested_command (with explicit position argument via properties);

of_properties: return filtered result;

added method encodeProperties; method command/ML: pass Properties; tuned error messages;

setting -H 2000 and no documents for higher performance;

add dcpo instance proof

declare upE as cases rule; add new rule up_induct

update sq_ord/po instance proofs

move lemmas from Cont.thy to Ffun.thy; reorder dependency of Cont.thy and Ffun.thy; add dcpo instance proofs for function type

remove not_up_less_UU [simp]

update instance proofs for sq_ord, po; new instance proofs for dcpo

add lemma ub2ub_monofun'

added dcpo instance proofs

new class dcpo; added dcpo versions of some lemmas

added new lemmas

add lemma dir2dir_monofun

tuned;

new is_ub lemmas; new lub syntax for set image

Multithreading.max_threads := 0 refers to number of cores of underlying machine;

added Multithreading.max_threads_value, which maps a value of 0 to number of CPUs;

added usedir -M max (alias for -M 0);

new section for directed sets

split of class uminus

empty dictionaries for OCaml

clarified policy

tuned

some more antiquotations

index now a copy of nat rather than int

absolute import

some more primrec

removed some legacy instantiations

improved evaluation mechanism

splitted class uminus from class minus

testing for empty sort

new metis proofs

renamed foldM to fold_mset on general request added Tobias' lemmas on fold_mset (A+B) etc tuned default simp set for fold_mset

update instance proofs to new style

declare sprodE as cases rule; new induction rule sprod_induct

add induction rule ssum_induct

eval_wrapper: CRITICAL; tuned;

try_ml_file: setmp explicit theory context, prevents race condition wrt. concurrent ML_Context.set_context;

tuned spaces;

removed separate exists/forall code;

tuned proofs and comments

removed obsolete banner;

tuned;

added PROMPT message;

added isSystem; tune isRaw;

simple make script;

tuned comments (javadoc);

use polyml-cvs, the 5.2 development branch;

tuned RandomWord interface;

added int/real/list operations; tuned interface; tuned;

use random_word.ML earlier;

changed type definition to make Iwhen and reasoning about chains unnecessary; rearranged sections

Fixed eta constraction issue in compose_witness

included meson/metis tests in simultaneous use_thys;

``print mode'' is now a thread-local value derived from a global template;

scheduling/next_task: PrintMode.closure;

added get/put_data;

separated into global template vs. thread-local value; made setmp thread-local (non-critical); added closure;

Universal values via tagged union. Emulates structure Universal in Poly/ML 5.1.

added ML-Systems/universal.ML;

updated;