2011-06-26 boehmes 2011-06-26 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
2011-06-25 wenzelm 2011-06-25 proper tokens only if session is ready;
2011-06-25 wenzelm 2011-06-25 entity markup for "type", "constant";
2011-06-25 wenzelm 2011-06-25 clarified Markup.CLASS vs. HTML.CLASS;
2011-06-25 wenzelm 2011-06-25 tuned color, to avoid confusion with type variables;
2011-06-25 wenzelm 2011-06-25 discontinued generic XML markup -- this is for XHTML with <span/> elements;
2011-06-25 wenzelm 2011-06-25 type classes: entity markup instead of old-style token markup;
2011-06-25 wenzelm 2011-06-25 clarified Binding.pretty/print: no quotes, only markup -- Binding.str_of is rendered obsolete;
2011-06-25 wenzelm 2011-06-25 clarified Binding.str_of/print: show full prefix + qualifier, which is relevant for print_locale, for example; discontinued unused Binding.qualified_name_of;
2011-06-25 wenzelm 2011-06-25 produce string constant directly;
2011-06-25 wenzelm 2011-06-25 merged
2011-06-25 ballarin 2011-06-25 While reading equations of an interpretation, already allow syntax provided by the interpretation base.
2011-06-25 wenzelm 2011-06-25 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;
2011-06-25 wenzelm 2011-06-25 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);
2011-06-25 wenzelm 2011-06-25 CLASSPATH already converted in isabelle java wrapper;
2011-06-25 wenzelm 2011-06-25 removed unused/broken Isabelle.exe for now -- needs update of Admin/launch4j;
2011-06-23 wenzelm 2011-06-23 more robust join_results: join_work needs to be uninterruptible, otherwise the task being dequeued by join_next might be never executed/finished!
2011-06-23 wenzelm 2011-06-23 clarified EXCEPTIONS [] (cf. Exn.is_interrupt and Runtime.exn_message);
2011-06-23 wenzelm 2011-06-23 more robust concurrent builds;
2011-06-23 huffman 2011-06-23 merged
2011-06-23 huffman 2011-06-23 add countable_datatype method for proving countable class instances
2011-06-23 wenzelm 2011-06-23 merged;
2011-06-23 huffman 2011-06-23 instance inat :: number_semiring
2011-06-23 huffman 2011-06-23 added number_semiring class, plus a few new lemmas; no changes to the simpset yet
2011-06-23 blanchet 2011-06-23 merged
2011-06-23 blanchet 2011-06-23 fiddle with remote ATP settings, based on Judgment Day
2011-06-23 blanchet 2011-06-23 give slightly more time to server to respond, to avoid leaving too much garbage on Geoff's servers
2011-06-23 ballarin 2011-06-23 Release notes should be written from the user's perspective. Don't assume the user has universal knowledge of the system.
2011-06-22 huffman 2011-06-22 generalize lemmas power_number_of_even and power_number_of_odd
2011-06-22 huffman 2011-06-22 merged
2011-06-22 huffman 2011-06-22 add HOLCF/ex/Concurrency_Monad.thy, which contains resumption/state/powerdomain monad example from my PhD thesis
2011-06-23 wenzelm 2011-06-23 simplified arrangement of jars;
2011-06-23 wenzelm 2011-06-23 adapted to Cygwin;
2011-06-23 wenzelm 2011-06-23 provide Isabelle/Scala environment as Java extension, instead of user classpath (which is subject to adhoc changes);
2011-06-23 wenzelm 2011-06-23 explicit import java.lang.System to prevent odd scope problems;
2011-06-23 wenzelm 2011-06-23 ensure export of initial CLASSPATH;
2011-06-23 wenzelm 2011-06-23 augment Java extension directories;
2011-06-23 wenzelm 2011-06-23 basic setup for Isabelle charset;
2011-06-22 wenzelm 2011-06-22 prefer actual charset over charset name;
2011-06-22 wenzelm 2011-06-22 clarified default ML settings;
2011-06-22 wenzelm 2011-06-22 lazy Isabelle_System.default supports implicit boot;
2011-06-22 wenzelm 2011-06-22 clarified plugin start/stop;
2011-06-22 wenzelm 2011-06-22 clarified init/exit procedure;
2011-06-22 wenzelm 2011-06-22 clarified decoded control symbols;
2011-06-22 wenzelm 2011-06-22 init/exit model/view synchronously within the swing thread -- EditBus.send in jedit-4.4.1 always runs there;
2011-06-22 wenzelm 2011-06-22 prefer STIXGeneral -- hard to tell if better or worse;
2011-06-22 wenzelm 2011-06-22 merged
2011-06-22 boehmes 2011-06-22 export lambda-lifting code as there is potential use for it within Sledgehammer
2011-06-22 wenzelm 2011-06-22 updated to jedit-4.4.1 and jedit_build-20110622;
2011-06-22 wenzelm 2011-06-22 clarified chunk.offset, chunk.length;
2011-06-21 wenzelm 2011-06-21 avoid fractional font metrics, which makes rendering really ugly (e.g. on Linux);
2011-06-21 wenzelm 2011-06-21 some arrow symbols from DejaVuSansMono for bsub/esub/bsup/esup;
2011-06-21 wenzelm 2011-06-21 more precise font transformations: shift sub/superscript, adjust size for user fonts; tuned;
2011-06-21 blanchet 2011-06-21 don't change the way helpers are generated for the exporter's sake
2011-06-21 blanchet 2011-06-21 provide appropriate type system and number of fact defaults for remote ATPs
2011-06-21 blanchet 2011-06-21 order generated facts topologically
2011-06-21 blanchet 2011-06-21 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")
2011-06-21 blanchet 2011-06-21 tweaked E, SPASS, Vampire setup based on latest Judgment Day results
2011-06-21 blanchet 2011-06-21 remove historical bloat -- another benefit of merging Metis's and Sledgehammer's translations
2011-06-21 blanchet 2011-06-21 avoid double ASCII-fication