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;
wenzelm [Wed, 02 Sep 2009 17:33:25 +0200] rev 32493
updated Poly/ML SVN version;
wenzelm [Wed, 02 Sep 2009 16:51:19 +0200] rev 32492
eval/location_props: always produce YXML markup, independent of print_mode;
wenzelm [Wed, 02 Sep 2009 16:25:44 +0200] rev 32491
reorganized Compute theories for HOL-Matrix -- avoiding theory files within main HOL/Tools;
wenzelm [Wed, 02 Sep 2009 14:11:45 +0200] rev 32490
tuned ML message;
nipkow [Wed, 02 Sep 2009 12:20:17 +0200] rev 32489
added "using" to blacklist