blanchet [Mon, 04 Aug 2014 12:28:42 +0200] rev 57776
rationalized sorting of facts -- so that preplaying (almost always) coincides with the real thing, preventing odd failures
blanchet [Mon, 04 Aug 2014 11:54:23 +0200] rev 57775
slightly earlier exit from preplaying
blanchet [Mon, 04 Aug 2014 11:43:19 +0200] rev 57774
honor 'dont_minimize' option when preplaying one-liner proof
sultana [Sun, 22 Jun 2014 06:16:57 +0100] rev 57773
Metis is being used to emulate E steps;
sultana [Sun, 22 Jun 2014 06:16:56 +0100] rev 57772
updated application of print_tac to take context parameter;
blanchet [Sat, 02 Aug 2014 00:15:08 +0200] rev 57771
better duplicate detection
blanchet [Fri, 01 Aug 2014 23:58:42 +0200] rev 57770
normalize conjectures vs. negated conjectures when comparing terms
blanchet [Fri, 01 Aug 2014 23:33:43 +0200] rev 57769
tweaked 'clone' formula detection
blanchet [Fri, 01 Aug 2014 23:29:50 +0200] rev 57768
fine-tuned Isar reconstruction, esp. boolean simplifications
blanchet [Fri, 01 Aug 2014 23:29:49 +0200] rev 57767
centralized boolean simplification so that e.g. LEO-II benefits from it