boehmes [Sat, 05 Sep 2009 11:45:57 +0200] rev 32521
added initialization and cleanup of actions,
added option to suppress Isabelle output,
sledgehammer action produces its own report (no need for additional perl script)
haftmann [Fri, 04 Sep 2009 15:19:51 +0200] rev 32520
merged
haftmann [Fri, 04 Sep 2009 15:18:35 +0200] rev 32519
tuned metis proofs
boehmes [Fri, 04 Sep 2009 13:57:56 +0200] rev 32518
tuned
nipkow [Fri, 04 Sep 2009 10:58:50 +0200] rev 32517
tuned output
boehmes [Thu, 03 Sep 2009 22:48:18 +0200] rev 32516
merged
boehmes [Thu, 03 Sep 2009 22:47:31 +0200] rev 32515
Mirabelle: actions are responsible for catching exceptions and producing suitable log messages (makes log message uniform),
removed PolyML.makestring (no strict dependency on PolyML anymore)
haftmann [Thu, 03 Sep 2009 20:26:07 +0200] rev 32514
merged
haftmann [Thu, 03 Sep 2009 17:26:10 +0200] rev 32513
merged
haftmann [Thu, 03 Sep 2009 15:39:02 +0200] rev 32512
proper class syntax for sublocale class < expr
boehmes [Thu, 03 Sep 2009 18:41:58 +0200] rev 32511
added option full_typed for sledgehammer action
boehmes [Thu, 03 Sep 2009 17:55:31 +0200] rev 32510
added runtime information to sledgehammer
boehmes [Thu, 03 Sep 2009 15:47:39 +0200] rev 32509
tuned
nipkow [Thu, 03 Sep 2009 15:30:05 +0200] rev 32508
scaled avg_time
nipkow [Thu, 03 Sep 2009 14:50:02 +0200] rev 32507
merged
nipkow [Thu, 03 Sep 2009 14:49:34 +0200] rev 32506
tuned
krauss [Thu, 03 Sep 2009 14:40:52 +0200] rev 32505
isatest: collect test results and logs in testdata repository
boehmes [Thu, 03 Sep 2009 14:31:04 +0200] rev 32504
replaced backlist by whitelist
boehmes [Thu, 03 Sep 2009 14:05:13 +0200] rev 32503
Mirabelle: logging of exceptions (works only for PolyML)
wenzelm [Wed, 02 Sep 2009 22:12:40 +0200] rev 32502
merged
wenzelm [Wed, 02 Sep 2009 22:12:20 +0200] rev 32501
refined delay into delay_first/delay_last;
boehmes [Wed, 02 Sep 2009 21:34:13 +0200] rev 32500
merged
boehmes [Wed, 02 Sep 2009 21:33:16 +0200] rev 32499
add report script for Mirabelle
boehmes [Wed, 02 Sep 2009 21:31:58 +0200] rev 32498
Mirabelle: actions are responsible for handling exceptions,
Mirabelle core logs only structural information,
measuring running times for sledgehammer and subsequent metis invocation,
Mirabelle produces reports for every theory (only for sledgehammer at the moment)
boehmes [Wed, 02 Sep 2009 16:29:50 +0200] rev 32497
removed errors overseen in previous changes
boehmes [Wed, 02 Sep 2009 16:23:53 +0200] rev 32496
moved Mirabelle from HOL/Tools to HOL,
added session HOL-Mirabelle
boehmes [Wed, 02 Sep 2009 16:02:37 +0200] rev 32495
removed unused signature
wenzelm [Wed, 02 Sep 2009 20:49:04 +0200] rev 32494
explicit checks;