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;

discontinued unused end_line, end_column;

more scalable HTML.output_width;

refined comment (again);

merged

use proper syntactic types for 'syntax' commands

make print translation for Abs_cfun consistent with other binders: prevent eta-contraction, but don't force eta-expansion

use full path for library imports

types -> type_synonym

updated NEOS_SERVER, which is now provided via settings;

renamed Sum_Of_Squares to Sum_of_Squares;

Ord_List.merge convenience;

misc tuning and comments based on review of Theory_Data, Proof_Data, Generic_Data usage;

modernized structure Prop_Logic; avoid ML structure aliases;

added Context_Position.is_visible_proof, which treats a global theory as invisible (unlike the default);

tuned;

tuned;

tuned headers;

merged

adding example theory for list comprehension to set comprehension simproc

adopting proofs due to new list comprehension to set comprehension simproc

adding simproc to rewrite list comprehensions to set comprehensions; adopting proofs

tuned text

merged

removing obselete Id comments from HOL/ex theories

added hints about licensing restrictions and how to enable Z3

tuned

eliminated hard tabs;

allow spaces in $SPASS_HOME value;

tuned;

eliminated alias;

do not open ML structures;

more standard package setup;