2012-04-24 sultana 2012-04-24 reversed Tools to Actions Mirabelle renaming;
2010-07-21 bulwahn 2010-07-21 fixing quickcheck invocation in HOL-Mirabelle
2009-09-13 wenzelm 2009-09-13 explicitly export type abbreviations (as usual in SML97); explicit type constraints for record patterns -- SML does not support record polymorphism; observe max. line length (80-100);
2009-09-12 wenzelm 2009-09-12 standard headers and text sections;
2009-09-05 boehmes 2009-09-05 added initialization and cleanup of actions, added option to suppress Isabelle output, sledgehammer action produces its own report (no need for additional perl script)
2009-09-04 boehmes 2009-09-04 tuned
2009-09-03 boehmes 2009-09-03 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)
2009-09-02 boehmes 2009-09-02 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)
2009-09-02 boehmes 2009-09-02 removed errors overseen in previous changes
2009-09-02 boehmes 2009-09-02 moved Mirabelle from HOL/Tools to HOL, added session HOL-Mirabelle