src/HOL/TPTP/MaSh_Eval.thy
Wed, 11 Dec 2013 18:02:22 +0100 wenzelm support for polml-5.5.2;
Tue, 19 Feb 2013 13:21:49 +0100 blanchet provide two modes for MaSh driver: linearized or real visibility
Thu, 17 Jan 2013 23:29:17 +0100 blanchet use precomputed MaSh/MePo data whenever available
Thu, 17 Jan 2013 18:53:13 +0100 blanchet provide a means to skip a method
Thu, 17 Jan 2013 18:43:59 +0100 blanchet evaluate more cases (cf. paper)
Thu, 17 Jan 2013 13:11:44 +0100 blanchet tweaked defaults
Sat, 15 Dec 2012 21:34:32 +0100 blanchet MaSh exporter can now export subsets of the facts, as consecutive ranges
Thu, 13 Dec 2012 22:49:06 +0100 blanchet parallelized MaSh exporter
Wed, 12 Dec 2012 21:59:03 +0100 blanchet tuning
Wed, 12 Dec 2012 00:24:06 +0100 blanchet adopt the neutral "prover" terminology for MaSh rather than the ambiguous/wrong ATP terminology (which sometimes excludes SMT solvers)
Mon, 10 Dec 2012 13:02:56 +0100 blanchet (re)introduce (even more) aggressive parallelism, for the benefit of those users with dozens of CPU cores
Mon, 10 Dec 2012 10:29:52 +0100 blanchet have MaSh evaluator keep all raw problem/solution files in a directory
Sat, 08 Dec 2012 00:48:50 +0100 blanchet store evaluation output in a file
Thu, 06 Dec 2012 16:07:09 +0100 blanchet use right names in MePo exporter
Tue, 04 Dec 2012 23:50:36 +0100 blanchet rationalized MaSh evaluation harness
Wed, 22 Aug 2012 22:55:41 +0200 wenzelm prefer ML_file over old uses;
Wed, 18 Jul 2012 08:44:05 +0200 blanchet repair MaSh exporter
Wed, 18 Jul 2012 08:44:04 +0200 blanchet fixed MaSh state load code so it works even if the facts are read in disorder
Wed, 18 Jul 2012 08:44:03 +0200 blanchet started implementing MaSh client-side I/O
Wed, 18 Jul 2012 08:44:03 +0200 blanchet renaming
less more (0) tip