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

remove automatic recovery from (some) unsound proofs, now that we use sound encodings for all the interesting provers

only refer to facts found in TPTP file -- e.g. facts that simplify to true are excluded

slightly better setup for E

respect "really_all" argument, which is used by "ATP_Export"

slightly better setup for SPASS and Vampire as more results have come in

optimized SPASS and Vampire time slices, like E before

optimized E's time slicing, based on latest exhaustive Judgment Day results

deal with ATP time slices in a more flexible/robust fashion

literal unicode in README.html allows to copy/paste from Lobo output;

merged;

explain special control symbols;