tuned signature;

more informative Build.build_results; tuned;

stop protocol handlers as well;

more robust command line -- accomodate /bin/kill on recent Linux (e.g. Xubuntu 13.04):

explicit management of Session.Protocol_Handlers, with protocol state and functions; more self-contained ML/Scala module Invoke_Scala;

prevent pretty printer from automatically annotating numerals

tuned

simplified example and proof

tuned

tuned messages;

proper options; tuned;

proper options;

more markup;

tuned;

less intrusive rendering of antiquoted text -- avoid visual clash with "blue variables" in particular;

proper context;

make SML/NJ happy;

added CASC-related files, to keep a public record of the Isabelle submission at the competition

disabled choice in Satallax

use HOL-TPTP image in TPTP tools (for less verbose and faster startup) and filter out some messages

prefer compiled version of LEO-II and Satallax if available

updated remote provers

added compatibility alias

merged

more rigorous check of simplifier context; tuned;

proper context;

proper context;

proper run-time context;

more precise treatment of theory vs. Proof.context;

proper run-time context;

tuned;

more explicit Session.update_options as source of Global_Options event;

even later Options.reset_default -- still needed for printing errors of Session.finish (e.g. via Command_Line.tool0);

tuned;

discontinued odd workaround for scala-2.9.2, which is hopefully obsolete in scala-2.10.x;

reset options last -- other parts of the system may still need them;

tuned signature;

updated Sledgehammer docs

parse agsyHOL proofs (as unsat cores)

freeze types in Sledgehammer goal, not just terms

generate agsyHOL-friendly THF (to some extent -- partial application of connectives remains an issue)

tuned code

started adding agsyHOL as an experimental prover

defined lvars and rvars of commands separately.

made "completish" mode a bit more complete

infrastructure for generic data for code symbols (constants, type constructors, classes, instances)

tuned and clarified

tuned, including signature

discontinued odd workaround for scala-2.10.0-RC1;

discontinued odd workaround for scala-2.9.2, which is hopefully obsolete in scala-2.10.x;

explicit notion of public options, which are shown in the editor options dialog; avoid hard-wired stuff;

back to more paranoid interrupt test after request is cancelled -- avoid race condition;

timeout counts as regular error, with rc = 1 (cf. special Exn.Interrupt vs. regular TimeLimit.TimeOut in Isabelle/ML);

added isabelle tty option -o;

oops;

renamed 'print_configs' to 'print_options';

proper option quick_and_dirty;

retain quick_and_dirty as-is -- no censorship;

more system-atic options;

added isabelle-process option -o;

more precise "eval", cf. isabelle build;

discontinued obsolete isabelle-process options -f and -u;

NEWS;

discontinued obsolete isabelle usedir, mkdir, make;

modernized TimeLimit.timeLimit using Event_Timer service -- based on more elementary version 11ae688e4e30;

event timer as separate service thread;

tuned signature;

tuned signature -- emphasize thread creation here;

repair after bc01725d7918;

replaced `;' by `;;' to disambiguate syntax; unexpected slight increase in build time

tuned

merged

more system options as context-sensitive config options;

Thy_Output.modes as proper option;

some system options as context-sensitive config options;

system options as context-sensitive configuration options within the attribute name space;

tuned signature;

properly handle SPASS constructors w.r.t. partially applied functions

tuned signature -- depend on context by default;

reflexivity rules for the function type and equality

tuned comments

correctly 'repair' the monomorphization context for SMT solvers from Sledgehammer

tuning

more work on SPASS datatypes

tuning -- renamed '_from_' to '_of_' in Sledgehammer

compile

don't recognize overloaded constants as constructors for the purpose of removing type arguments

tuning

reintroduced syntax for "nonexhaustive" datatypes

tuning

more work on SPASS datatypes

merged

setup for set membership as a predicate for code_pred

tuned

explicitly state equivalence relation for sim; tweak syntax of sem_equiv

merged

finally: acom with pointwise access and update of annotations

merged;

clarified preferences: "override" re-initialized on prover startup, and "default" sent to PG -- thus recover typical defaults like auto-quickcheck in PG 4.x;

simplified ProofGeneral.preference operation -- no need for CRITICAL section for atomic access (and sequential execution of PG/TTY loop);

back to hidden welcome -- revert change 9ebf2da69b29, which appears to disturb startup protocol of PG 4.1;

more standard Isabelle/ML structures for global preferences; allow to add categories later on; allow to redefine preferences as usual for global tables, e.g. after reloading ML modules;

more basic print mode "ProofGeneral" (again);

uniform welcome -- actually visible on startup via Output.urgent_message; tuned;

more elementary ProofGeneral.thm_deps;

tuned;

moved files;

clarified default for Proofterm.proofs, according to etc/options and innermost setmp;

maintain ProofGeneral preferences within ProofGeneral module; initialize Isabelle/Pure preferences within normal user space (with antiquotations); tuned;

just one ProofGeneral module;

tuning

more work on SPASS datatypes