boehmes [Sun, 26 Jun 2011 19:10:02 +0200] rev 43554
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
wenzelm [Sat, 25 Jun 2011 20:03:07 +0200] rev 43553
proper tokens only if session is ready;
wenzelm [Sat, 25 Jun 2011 19:38:35 +0200] rev 43552
entity markup for "type", "constant";
wenzelm [Sat, 25 Jun 2011 19:19:13 +0200] rev 43551
clarified Markup.CLASS vs. HTML.CLASS;
wenzelm [Sat, 25 Jun 2011 18:29:51 +0200] rev 43550
tuned color, to avoid confusion with type variables;
wenzelm [Sat, 25 Jun 2011 18:24:52 +0200] rev 43549
discontinued generic XML markup -- this is for XHTML with <span/> elements;
wenzelm [Sat, 25 Jun 2011 18:15:36 +0200] rev 43548
type classes: entity markup instead of old-style token markup;
wenzelm [Sat, 25 Jun 2011 17:17:49 +0200] rev 43547
clarified Binding.pretty/print: no quotes, only markup -- Binding.str_of is rendered obsolete;
wenzelm [Sat, 25 Jun 2011 15:08:58 +0200] rev 43546
clarified Binding.str_of/print: show full prefix + qualifier, which is relevant for print_locale, for example;
discontinued unused Binding.qualified_name_of;
wenzelm [Sat, 25 Jun 2011 15:02:12 +0200] rev 43545
produce string constant directly;
wenzelm [Sat, 25 Jun 2011 14:28:43 +0200] rev 43544
merged
ballarin [Sat, 25 Jun 2011 12:19:54 +0200] rev 43543
While reading equations of an interpretation, already allow syntax provided by the interpretation base.
wenzelm [Sat, 25 Jun 2011 14:25:10 +0200] rev 43542
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;
wenzelm [Sat, 25 Jun 2011 12:57:46 +0200] rev 43541
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);
wenzelm [Sat, 25 Jun 2011 12:54:32 +0200] rev 43540
CLASSPATH already converted in isabelle java wrapper;
wenzelm [Sat, 25 Jun 2011 11:51:50 +0200] rev 43539
removed unused/broken Isabelle.exe for now -- needs update of Admin/launch4j;
wenzelm [Thu, 23 Jun 2011 23:12:00 +0200] rev 43538
more robust join_results: join_work needs to be uninterruptible, otherwise the task being dequeued by join_next might be never executed/finished!
wenzelm [Thu, 23 Jun 2011 23:05:38 +0200] rev 43537
clarified EXCEPTIONS [] (cf. Exn.is_interrupt and Runtime.exn_message);
wenzelm [Thu, 23 Jun 2011 20:30:48 +0200] rev 43536
more robust concurrent builds;
huffman [Thu, 23 Jun 2011 10:08:35 -0700] rev 43535
merged
huffman [Thu, 23 Jun 2011 10:07:16 -0700] rev 43534
add countable_datatype method for proving countable class instances
wenzelm [Thu, 23 Jun 2011 18:32:13 +0200] rev 43533
merged;
huffman [Thu, 23 Jun 2011 09:16:48 -0700] rev 43532
instance inat :: number_semiring
huffman [Thu, 23 Jun 2011 09:04:20 -0700] rev 43531
added number_semiring class, plus a few new lemmas;
no changes to the simpset yet
blanchet [Thu, 23 Jun 2011 16:31:20 +0200] rev 43530
merged
blanchet [Thu, 23 Jun 2011 11:19:41 +0200] rev 43529
fiddle with remote ATP settings, based on Judgment Day
blanchet [Thu, 23 Jun 2011 11:19:41 +0200] rev 43528
give slightly more time to server to respond, to avoid leaving too much garbage on Geoff's servers
ballarin [Thu, 23 Jun 2011 12:02:54 +0200] rev 43527
Release notes should be written from the user's perspective. Don't assume the user has universal knowledge of the system.
huffman [Wed, 22 Jun 2011 15:58:55 -0700] rev 43526
generalize lemmas power_number_of_even and power_number_of_odd
huffman [Wed, 22 Jun 2011 13:45:32 -0700] rev 43525
merged