tuned;

misc tuning for release;

merged

Tuned show_status

proper type variables with sorts;

non-executable sources;

tuned headers;

tuned;

type_synonym;

more standard command descriptions;

added before_exit continuation for named targets (locale, class etc.), e.g. for final check/cleanup as in VC management;

Replaced ad-hoc advance function by Position.advance

merged

experimental variant of interpretation with simultaneous definitions, plus example

clarified pretty_statement: more robust treatment of fixes and conclusion of elimination (e.g. for classical rule);

link HOL-Proofs/index.html, which is not reachable from regular HOL/index.html;

type_synonym;

recovered printing of record updates over compound terms, e.g. "(|x = a|)(|x := b|)", which was apparently broken in 45a2ffc5911e; tuned;

export Record.get_hierarchy -- external tools typically need this information;

tuned;

removed unreferenced identifiers;

global "prems" is legacy feature;

misc updates for release;

merged;

misc tuning for release;

normalize Z3 models: assignments to free variables should ideally not refer to other free variables

Also added SPARK to test and clean targets.

merged

Added entry for HOL-SPARK

Added HOL-SPARK and removed old_primrec.ML

unused_thms no longer compares propositions, since this is no longer needed and did not work properly any longer after the addition of class constraints to propositions.

Include HOL-SPARK keywords

Include HOL-SPARK

Finally removed old primrec package, since Primrec.add_primrec_global can be used instead.

Added new SPARK verification environment.

remove presently unused Isabelle application for official releases;

hardwired default for proof-shell-quit-timeout (PG 4.1 provides rather low value);

treat HOLCF as HOL library session, not as "logic";

increased startup-timeout to accommodate slow systems (especially Windows/Cygwin);

bundle main HOL image only, to save about 300 MB disk space;

updated for release;

adjusted mira configuration

merged

global "prems" is legacy feature;

tuned markup;

eliminated global prems; tuned proofs;

more precise import; eliminated global prems;

Thy_Load.begin_theory: maintain source specification of imports; Thy_Info.register_thy: reconstruct deps using original imports (important for ProofGeneral.inform_file_processed);

merged

integral on lebesgue measure is extension of integral on borel measure

tuned formalization of subalgebra

introduced integral syntax

tuned theorem order

configuration file for mira

eliminated global prems; tuned proofs;

more precise pretty printing -- to accomodate Scala message layout;

less verbosity -- avoid slightly odd tracing information on warning channel;

updated Isabelle/jEdit limitations and workarounds;

full theory path enables loading parents via master directory and keeps files strictly separate;

Toplevel.init_theory: maintain optional master directory, to allow bypassing global Thy_Load.master_path;

clarified split_thy_path;

less verbosity;

proper 'domain' class instance for 'a defl, with deflation combinator

documented Option.bind

CONTRIBUTORS

updated keywords;

eliminated global prems;

eliminated global prems; tuned proofs;

updated to ProofGeneral-4.x;

eliminated global prems;

tuned proof;

eliminated global prems; tuned proofs;

compile;

more FIXMEs concerning bad catch-all exception handlers;

eliminated obsolete print_sign_exn_unit;

reraise interrupts as usual;

avoid catch-all exception handler, presumably TERM was meant here;

disabled experimental treatment of replacement text for now, which leads to odd spacing and strange effects on non-poppler viewers;

observe line length limit;

smart_string_of_real: print integer values without fractional part;

tuned (cf. 2fe62d602681);

added dist/jedit symlink for convenience;

record versions of both jEdit and Isabelle;

updated to Isabelle2011;

isabelle version -i;

NEWS

NEWS

eliminated duplication

merged

tuned text

"enriched_type" replaces less specific "type_lifting"

clarified notion Position.is_reported; ML warning/error: retain non-reported clear-text position, notably when evaluating external ML files;

refined report_parse_tree: reverse reports happen to produce proper type information for inlined @{term}, @{typ} etc.; tuned offset_position_of;

refined ML_Lex.flatten: ensure proper separation of tokens;

ML compiler: more careful treatment of input tokens -- trailing space ensures proper separation and end position (cf. 82c1e348bc18, 08240feb69c7);

use just one data slot to VC-related information

be more precise: also merge option values

only print warning in a visible context (previously, the warning was printed more than once)

dropped superfluous error message

removed obsolete make target (now in doc-src, cf. 28b487cd9e15)

updated for polyml-5.4.0; discontinued old-fashioned POLY_HOME via path; more robust handling of polyml-version, preferably provided by Poly/ML distribution itself;

made SML/NJ happy;

added merge_options convenience;

tuned string_of_int to avoid allocation for small integers;

eliminated Int.toString;

eliminated obsolete LargeInt -- Int is unbounded;

standardized split_last/last_elem towards List.last; eliminated obsolete Library.last_elem;

removing dead code; tuned

made SML/NJ happy

reverted 08240feb69c7 -- breaks positions of reports;

ML_trace: observe context visibility flag (import for Latex mode, for example);

more direct treatment of Position.end_offset; tuned;