2011-03-20 ago structure Timing: covers former start_timing/end_timing and Output.timeit etc;
2011-01-09 ago refined comment (again);
2011-01-08 ago misc tuning and comments based on review of Theory_Data, Proof_Data, Generic_Data usage;
2010-09-20 ago renamed structure PureThy to Pure_Thy and moved most content to Global_Theory, to emphasize that this is global-only;
2010-09-16 ago prevent exception when calling "Mirabelle.can_apply" on empty proof sequence;
2010-09-14 ago tuning
2010-09-09 ago more abstract treatment of interrupts in structure Exn -- hardly ever need to mention Interrupt literally;
2010-05-10 ago renamed Config.get_thy to Config.get_global etc. to indicate that this is not the real thing;
2010-03-28 ago static defaults for configuration options;
2010-03-05 ago use regular Proof.goal (which is what methods usually see) and prevent sledgehammer from crashing;
2009-12-10 ago only invoke metisFT if metis failed
2009-12-08 ago also consider the fully-typed version of metis for Mirabelle measurements
2009-11-08 ago adapted Theory_Data;
2009-10-28 ago renamed raw Proof.get_goal to Proof.raw_goal;
2009-10-27 ago normalized basic type abbreviations;
2009-09-24 ago record how many "proof"s are solved by s/h
2009-09-13 ago explicitly export type abbreviations (as usual in SML97);
2009-09-12 ago standard headers and text sections;
2009-09-10 ago position information is now passed to all actions;
2009-09-05 ago added initialization and cleanup of actions,
2009-09-03 ago Mirabelle: actions are responsible for catching exceptions and producing suitable log messages (makes log message uniform),
2009-09-03 ago replaced backlist by whitelist
2009-09-03 ago Mirabelle: logging of exceptions (works only for PolyML)
2009-09-02 ago Mirabelle: actions are responsible for handling exceptions,
2009-09-02 ago removed errors overseen in previous changes
2009-09-02 ago moved Mirabelle from HOL/Tools to HOL,