CLASSPATH already converted in isabelle java wrapper;

removed unused/broken Isabelle.exe for now -- needs update of Admin/launch4j;

more robust join_results: join_work needs to be uninterruptible, otherwise the task being dequeued by join_next might be never executed/finished!

clarified EXCEPTIONS [] (cf. Exn.is_interrupt and Runtime.exn_message);

more robust concurrent builds;

merged

add countable_datatype method for proving countable class instances

merged;

instance inat :: number_semiring

added number_semiring class, plus a few new lemmas; no changes to the simpset yet

merged

fiddle with remote ATP settings, based on Judgment Day

give slightly more time to server to respond, to avoid leaving too much garbage on Geoff's servers

Release notes should be written from the user's perspective. Don't assume the user has universal knowledge of the system.

generalize lemmas power_number_of_even and power_number_of_odd

merged

add HOLCF/ex/Concurrency_Monad.thy, which contains resumption/state/powerdomain monad example from my PhD thesis

simplified arrangement of jars;

adapted to Cygwin;

provide Isabelle/Scala environment as Java extension, instead of user classpath (which is subject to adhoc changes);

explicit import java.lang.System to prevent odd scope problems;

ensure export of initial CLASSPATH;

augment Java extension directories;

basic setup for Isabelle charset;

prefer actual charset over charset name;

clarified default ML settings;

lazy Isabelle_System.default supports implicit boot;

clarified plugin start/stop;

clarified init/exit procedure;

clarified decoded control symbols;

init/exit model/view synchronously within the swing thread -- EditBus.send in jedit-4.4.1 always runs there;

prefer STIXGeneral -- hard to tell if better or worse;

merged

export lambda-lifting code as there is potential use for it within Sledgehammer

updated to jedit-4.4.1 and jedit_build-20110622;

clarified chunk.offset, chunk.length;

avoid fractional font metrics, which makes rendering really ugly (e.g. on Linux);

some arrow symbols from DejaVuSansMono for bsub/esub/bsup/esup;

more precise font transformations: shift sub/superscript, adjust size for user fonts; tuned;

don't change the way helpers are generated for the exporter's sake

provide appropriate type system and number of fact defaults for remote ATPs

order generated facts topologically

peel off two or more layers in exceptional cases where the proof term refers to the proved theorems twice with the same name (e.g., "Transitive_Closure.trancl_into_trancl")

tweaked E, SPASS, Vampire setup based on latest Judgment Day results

remove historical bloat -- another benefit of merging Metis's and Sledgehammer's translations

avoid double ASCII-fication

make sure that enough type information is generated -- because the exported "lemma"s are also used as "conjecture", we can't optimize type information based on polarity

generate type predicates for existentials/skolems, otherwise some problems might not be provable

insert rather than append special facts to make it less likely that they're truncated away

hidden font: full height makes cursor more visible;

more uniform treatment of recode_set/recode_map; HTML spans with user fonts;

tuned iteration over short symbols;

Symbol.is_ctrl: handle decoded version as well; clarified user font font index handling;

some support for user symbol fonts;

removed obsolete font specification;

more tolerant Symbol.decode;

simplified/generalized ISABELLE_FONTS handling;

updated to jedit_build-20110620;

added SyntaxUtilities.StyleExtender hook, with actual functionality in Isabelle/Scala;

clean up SPASS FLOTTER hack