Mon, 27 Jun 2011 14:56:33 +0200 don't export any metastrange or other nonatomizable formulas, since these don't help proving normal things, they are somewhat broken in the ATP output, and they are atypical
blanchet [Mon, 27 Jun 2011 14:56:33 +0200] rev 43576
don't export any metastrange or other nonatomizable formulas, since these don't help proving normal things, they are somewhat broken in the ATP output, and they are atypical
Mon, 27 Jun 2011 14:56:32 +0200 tweaked comment
blanchet [Mon, 27 Jun 2011 14:56:32 +0200] rev 43575
tweaked comment
Mon, 27 Jun 2011 14:56:31 +0200 document "sound" option
blanchet [Mon, 27 Jun 2011 14:56:31 +0200] rev 43574
document "sound" option
Mon, 27 Jun 2011 14:56:29 +0200 minor Sledgehammer news
blanchet [Mon, 27 Jun 2011 14:56:29 +0200] rev 43573
minor Sledgehammer news
Mon, 27 Jun 2011 14:56:28 +0200 added "sound" option to force Sledgehammer to be pedantically sound
blanchet [Mon, 27 Jun 2011 14:56:28 +0200] rev 43572
added "sound" option to force Sledgehammer to be pedantically sound
Mon, 27 Jun 2011 14:56:26 +0200 removed "full_types" option from documentation
blanchet [Mon, 27 Jun 2011 14:56:26 +0200] rev 43571
removed "full_types" option from documentation
Mon, 27 Jun 2011 14:56:10 +0200 document changes to Sledgehammer and "try"
blanchet [Mon, 27 Jun 2011 14:56:10 +0200] rev 43570
document changes to Sledgehammer and "try"
Mon, 27 Jun 2011 13:52:47 +0200 removed "full_types" option from Sledgehammer, now that virtually sound encodings are used as the default anyway
blanchet [Mon, 27 Jun 2011 13:52:47 +0200] rev 43569
removed "full_types" option from Sledgehammer, now that virtually sound encodings are used as the default anyway
Mon, 27 Jun 2011 13:52:47 +0200 clarify warning message to avoid confusing beginners
blanchet [Mon, 27 Jun 2011 13:52:47 +0200] rev 43568
clarify warning message to avoid confusing beginners
Mon, 27 Jun 2011 13:52:47 +0200 remove experimental trimming feature -- it slowed down things on Linux for some reason
blanchet [Mon, 27 Jun 2011 13:52:47 +0200] rev 43567
remove experimental trimming feature -- it slowed down things on Linux for some reason
Mon, 27 Jun 2011 13:52:47 +0200 filter out some tautologies using an ATP, especially for those theories that are known for producing such things
blanchet [Mon, 27 Jun 2011 13:52:47 +0200] rev 43566
filter out some tautologies using an ATP, especially for those theories that are known for producing such things
Mon, 27 Jun 2011 22:23:44 +0200 NEWS;
wenzelm [Mon, 27 Jun 2011 22:23:44 +0200] rev 43565
NEWS;
Mon, 27 Jun 2011 22:20:49 +0200 document antiquotations are managed as theory data, with proper name space and entity markup;
wenzelm [Mon, 27 Jun 2011 22:20:49 +0200] rev 43564
document antiquotations are managed as theory data, with proper name space and entity markup;
Mon, 27 Jun 2011 17:51:28 +0200 proper checking of @{ML_antiquotation};
wenzelm [Mon, 27 Jun 2011 17:51:28 +0200] rev 43563
proper checking of @{ML_antiquotation};
Mon, 27 Jun 2011 17:20:24 +0200 hide rather short auxiliary names, which can easily occur in user theories;
wenzelm [Mon, 27 Jun 2011 17:20:24 +0200] rev 43562
hide rather short auxiliary names, which can easily occur in user theories;
Mon, 27 Jun 2011 17:06:06 +0200 updated generated file;
wenzelm [Mon, 27 Jun 2011 17:06:06 +0200] rev 43561
updated generated file;
Mon, 27 Jun 2011 16:53:31 +0200 ML antiquotations are managed as theory data, with proper name space and entity markup;
wenzelm [Mon, 27 Jun 2011 16:53:31 +0200] rev 43560
ML antiquotations are managed as theory data, with proper name space and entity markup; clarified Name_Space.check;
Mon, 27 Jun 2011 15:03:55 +0200 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: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;
Mon, 27 Jun 2011 15:01:08 +0200 parallel Syntax.parse, which is rather slow;
wenzelm [Mon, 27 Jun 2011 15:01:08 +0200] rev 43558
parallel Syntax.parse, which is rather slow;
Mon, 27 Jun 2011 14:38:58 +0200 markup binding like class, which is the only special markup where Proof General (including version 4.1) allows "isar-long-id-stuff";
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";
Mon, 27 Jun 2011 09:42:46 +0200 move conditional expectation to its own theory file
hoelzl [Mon, 27 Jun 2011 09:42:46 +0200] rev 43556
move conditional expectation to its own theory file
Sun, 26 Jun 2011 19:10:03 +0200 updated SMT certificates
boehmes [Sun, 26 Jun 2011 19:10:03 +0200] rev 43555
updated SMT certificates
Sun, 26 Jun 2011 19:10:02 +0200 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);
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
Sat, 25 Jun 2011 20:03:07 +0200 proper tokens only if session is ready;
wenzelm [Sat, 25 Jun 2011 20:03:07 +0200] rev 43553
proper tokens only if session is ready;
Sat, 25 Jun 2011 19:38:35 +0200 entity markup for "type", "constant";
wenzelm [Sat, 25 Jun 2011 19:38:35 +0200] rev 43552
entity markup for "type", "constant";
Sat, 25 Jun 2011 19:19:13 +0200 clarified Markup.CLASS vs. HTML.CLASS;
wenzelm [Sat, 25 Jun 2011 19:19:13 +0200] rev 43551
clarified Markup.CLASS vs. HTML.CLASS;
Sat, 25 Jun 2011 18:29:51 +0200 tuned color, to avoid confusion with type variables;
wenzelm [Sat, 25 Jun 2011 18:29:51 +0200] rev 43550
tuned color, to avoid confusion with type variables;
Sat, 25 Jun 2011 18:24:52 +0200 discontinued generic XML markup -- this is for XHTML with <span/> elements;
wenzelm [Sat, 25 Jun 2011 18:24:52 +0200] rev 43549
discontinued generic XML markup -- this is for XHTML with <span/> elements;
Sat, 25 Jun 2011 18:15:36 +0200 type classes: entity markup instead of old-style token markup;
wenzelm [Sat, 25 Jun 2011 18:15:36 +0200] rev 43548
type classes: entity markup instead of old-style token markup;
Sat, 25 Jun 2011 17:17:49 +0200 clarified Binding.pretty/print: no quotes, only markup -- Binding.str_of is rendered obsolete;
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;
(0) -30000 -10000 -3000 -1000 -300 -100 -50 -30 +30 +50 +100 +300 +1000 +3000 +10000 +30000 tip