Sat, 25 Jun 2011 12:54:32 +0200 wenzelm CLASSPATH already converted in isabelle java wrapper;
Sat, 25 Jun 2011 11:51:50 +0200 wenzelm removed unused/broken Isabelle.exe for now -- needs update of Admin/launch4j;
Thu, 23 Jun 2011 23:12:00 +0200 wenzelm more robust join_results: join_work needs to be uninterruptible, otherwise the task being dequeued by join_next might be never executed/finished!
Thu, 23 Jun 2011 23:05:38 +0200 wenzelm clarified EXCEPTIONS [] (cf. Exn.is_interrupt and Runtime.exn_message);
Thu, 23 Jun 2011 20:30:48 +0200 wenzelm more robust concurrent builds;
Thu, 23 Jun 2011 10:08:35 -0700 huffman merged
Thu, 23 Jun 2011 10:07:16 -0700 huffman add countable_datatype method for proving countable class instances
Thu, 23 Jun 2011 18:32:13 +0200 wenzelm merged;
Thu, 23 Jun 2011 09:16:48 -0700 huffman instance inat :: number_semiring
Thu, 23 Jun 2011 09:04:20 -0700 huffman added number_semiring class, plus a few new lemmas;
Thu, 23 Jun 2011 16:31:20 +0200 blanchet merged
Thu, 23 Jun 2011 11:19:41 +0200 blanchet fiddle with remote ATP settings, based on Judgment Day
Thu, 23 Jun 2011 11:19:41 +0200 blanchet give slightly more time to server to respond, to avoid leaving too much garbage on Geoff's servers
Thu, 23 Jun 2011 12:02:54 +0200 ballarin Release notes should be written from the user's perspective. Don't assume the user has universal knowledge of the system.
Wed, 22 Jun 2011 15:58:55 -0700 huffman generalize lemmas power_number_of_even and power_number_of_odd
Wed, 22 Jun 2011 13:45:32 -0700 huffman merged
Wed, 22 Jun 2011 13:30:28 -0700 huffman add HOLCF/ex/Concurrency_Monad.thy, which contains resumption/state/powerdomain monad example from my PhD thesis
Thu, 23 Jun 2011 17:17:40 +0200 wenzelm simplified arrangement of jars;
Thu, 23 Jun 2011 16:34:29 +0200 wenzelm adapted to Cygwin;
Thu, 23 Jun 2011 16:10:22 +0200 wenzelm provide Isabelle/Scala environment as Java extension, instead of user classpath
Thu, 23 Jun 2011 14:52:32 +0200 wenzelm explicit import java.lang.System to prevent odd scope problems;
Thu, 23 Jun 2011 14:48:32 +0200 wenzelm ensure export of initial CLASSPATH;
Thu, 23 Jun 2011 13:23:00 +0200 wenzelm augment Java extension directories;
Thu, 23 Jun 2011 10:58:29 +0200 wenzelm basic setup for Isabelle charset;
Wed, 22 Jun 2011 23:56:44 +0200 wenzelm prefer actual charset over charset name;
Wed, 22 Jun 2011 21:54:35 +0200 wenzelm clarified default ML settings;
Wed, 22 Jun 2011 21:35:48 +0200 wenzelm lazy Isabelle_System.default supports implicit boot;
Wed, 22 Jun 2011 21:27:20 +0200 wenzelm clarified plugin start/stop;
Wed, 22 Jun 2011 20:56:18 +0200 wenzelm clarified init/exit procedure;
Wed, 22 Jun 2011 20:38:03 +0200 wenzelm clarified decoded control symbols;
Wed, 22 Jun 2011 20:25:35 +0200 wenzelm init/exit model/view synchronously within the swing thread -- EditBus.send in jedit-4.4.1 always runs there;
Wed, 22 Jun 2011 20:21:22 +0200 wenzelm prefer STIXGeneral -- hard to tell if better or worse;
Wed, 22 Jun 2011 16:35:31 +0200 wenzelm merged
Wed, 22 Jun 2011 15:07:03 +0200 boehmes export lambda-lifting code as there is potential use for it within Sledgehammer
Wed, 22 Jun 2011 16:32:36 +0200 wenzelm updated to jedit-4.4.1 and jedit_build-20110622;
Wed, 22 Jun 2011 16:01:30 +0200 wenzelm clarified chunk.offset, chunk.length;
Tue, 21 Jun 2011 23:08:16 +0200 wenzelm avoid fractional font metrics, which makes rendering really ugly (e.g. on Linux);
Tue, 21 Jun 2011 22:40:30 +0200 wenzelm some arrow symbols from DejaVuSansMono for bsub/esub/bsup/esup;
Tue, 21 Jun 2011 21:34:36 +0200 wenzelm more precise font transformations: shift sub/superscript, adjust size for user fonts;
Tue, 21 Jun 2011 17:17:39 +0200 blanchet don't change the way helpers are generated for the exporter's sake
Tue, 21 Jun 2011 17:17:39 +0200 blanchet provide appropriate type system and number of fact defaults for remote ATPs
Tue, 21 Jun 2011 17:17:39 +0200 blanchet order generated facts topologically
Tue, 21 Jun 2011 17:17:39 +0200 blanchet 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")
Tue, 21 Jun 2011 17:17:39 +0200 blanchet tweaked E, SPASS, Vampire setup based on latest Judgment Day results
Tue, 21 Jun 2011 17:17:39 +0200 blanchet remove historical bloat -- another benefit of merging Metis's and Sledgehammer's translations
Tue, 21 Jun 2011 17:17:39 +0200 blanchet avoid double ASCII-fication
Tue, 21 Jun 2011 17:17:39 +0200 blanchet 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
Tue, 21 Jun 2011 17:17:39 +0200 blanchet generate type predicates for existentials/skolems, otherwise some problems might not be provable
Tue, 21 Jun 2011 17:17:38 +0200 blanchet insert rather than append special facts to make it less likely that they're truncated away
Tue, 21 Jun 2011 15:43:27 +0200 wenzelm hidden font: full height makes cursor more visible;
Tue, 21 Jun 2011 14:12:49 +0200 wenzelm more uniform treatment of recode_set/recode_map;
Tue, 21 Jun 2011 13:29:44 +0200 wenzelm tuned iteration over short symbols;
Tue, 21 Jun 2011 12:53:55 +0200 wenzelm Symbol.is_ctrl: handle decoded version as well;
Tue, 21 Jun 2011 01:08:15 +0200 wenzelm some support for user symbol fonts;
Mon, 20 Jun 2011 23:25:39 +0200 wenzelm removed obsolete font specification;
Mon, 20 Jun 2011 23:21:24 +0200 wenzelm more tolerant Symbol.decode;
Mon, 20 Jun 2011 23:19:38 +0200 wenzelm simplified/generalized ISABELLE_FONTS handling;
Mon, 20 Jun 2011 22:48:41 +0200 wenzelm updated to jedit_build-20110620;
Mon, 20 Jun 2011 22:43:56 +0200 wenzelm added SyntaxUtilities.StyleExtender hook, with actual functionality in Isabelle/Scala;
Mon, 20 Jun 2011 12:13:43 +0200 blanchet clean up SPASS FLOTTER hack
(0) -30000 -10000 -3000 -1000 -300 -100 -60 +60 +100 +300 +1000 +3000 +10000 +30000 tip