wenzelm [Mon, 27 Jun 2011 15:03:55 +0200] rev 43559
old gensym is now legacy -- global state is out of fashion, and its result is not guaranteed to be fresh;
wenzelm [Mon, 27 Jun 2011 15:01:08 +0200] rev 43558
parallel Syntax.parse, which is rather slow;
wenzelm [Mon, 27 Jun 2011 14:38:58 +0200] rev 43557
markup binding like class, which is the only special markup where Proof General (including version 4.1) allows "isar-long-id-stuff";
hoelzl [Mon, 27 Jun 2011 09:42:46 +0200] rev 43556
move conditional expectation to its own theory file
boehmes [Sun, 26 Jun 2011 19:10:03 +0200] rev 43555
updated SMT certificates
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