updated SMT certificates

generalized introduction of explicit application constant: consider more functions as possible witness/instance of quantifiers than before (a constant of type T1 -> T2 -> T3 should be considered to have a rank less or equal to 1 if variables of type T2 -> T3 occur bound in a problem); maintain extra-logical information when introducing explicit application; handle let-expressions properly

proper tokens only if session is ready;

entity markup for "type", "constant";

clarified Markup.CLASS vs. HTML.CLASS;

tuned color, to avoid confusion with type variables;

discontinued generic XML markup -- this is for XHTML with <span/> elements;

type classes: entity markup instead of old-style token markup;

clarified Binding.pretty/print: no quotes, only markup -- Binding.str_of is rendered obsolete;

clarified Binding.str_of/print: show full prefix + qualifier, which is relevant for print_locale, for example; discontinued unused Binding.qualified_name_of;

produce string constant directly;

merged

While reading equations of an interpretation, already allow syntax provided by the interpretation base.

removed very slow proof of unnamed/unused theorem from HOL/Quickcheck_Narrowing.thy (cf. 2dee03f192b7) -- can take seconds for main HOL and minutes for HOL-Proofs;

clarified java.ext.dirs: putting Isabelle extensions first makes it work miraculously even on Cygwin with Java in "C:\Program Files\..." (with spaces in file name);

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