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;