adhoc patches relative to ProofGeneral-4.1pre101216, which has setprefs working;

more precise stats;

some adhoc patches for ProofGeneral-4.1pre110112;

enforce STIXGeneral, which is preferred by PG 4.1;

default UTF-8 locale, to work with funny base directory (e.g. Chinese);

enforce fonts;

added option -f FONT;

Proof General 4.x interface wrapper;

old Proof General patches;

Added tag isa2011-test3 for changeset 55a45051b220

Tuned definition of sdiv.

CRITICAL markup for critical poking with unsynchronized references;

Replaced smod by standard mod operator to reflect actual behaviour of the SPARK tools.

cancel document execution before editing, to improve reactivity on systems with few cores;

tuned isatest settings (for Poly/ML SVN 1278);

merged

do not restore old files on startup, which is potentially slow due to automatic rechecking; attempt to enable thick caret for improved visibility;

singleton (sequential) execution, to avoid race conditions in theory loader state (e.g. when multiple independent theories import the same theory);

workaround for odd x86_64 problem in Poly/ML 5.4.0 (actually SVN 1151?), which causes unexpected nontermination of Isabelle/Scala document editing;

improved README -- Isabelle symbols and fonts;

delete compiled .elc files to improve portability on Linux, notably for GNU Emacs 23.1.x instead of 23.2.x;

do not overwrite proof-shell-quit-timeout by default (final PG 4.1 supposedly gets it right);

Added tag isa2011-test2 for changeset 237328506a42

Documented unused_thms

JVM/Windows: more robust treatment of unicode in file names;

java/scala: default to UTF-8;

updated Named_Target.init;

made SML/NJ happy;

Word: direct conversion wrt. LargeInt to bypass exception Overflow;

fixing list_to_set_comprehension simproc

more release checks;

potentially more robust utf8 handling (cf. 3e4bb6e7c3ca);

clasrified classpath: add in front in accordance to librarypath (cf. b7cd80330a16), for slightly more robustness;

added librarypath: shared library convenience in bash, keeping LD_LIBRARY_PATH and DYLD_LIBRARY_PATH separate;

merged

tuned;

Cygwin: back to ProofGeneral-3.7.1.1 with XEmacs, since PG 4.x with GNU Emacs 23 is painfully slow;

isabelle jedit as alternative;

Apple's way of locating java;

more notes on final release stage;

makedist: refer to isabelle-release;

Added tag isa2011-test1 for changeset 7d035da21e9c

tuned;

some announcement;

tuned;

merged

made Z3 the default SMT solver again

some notes on final release stage;

isatest: run at-poly on macbroy28 for slightly more robust isatest-doc;

keep Proof General 4.0 and 3.7.1.1 for now;

tuned;

misc updates for release;

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;