blanchet [Mon, 23 Jul 2012 15:32:30 +0200] rev 48440
identified "evil" theories for MaSh -- this is rather ad hoc, but so is MaSh anyway
blanchet [Mon, 23 Jul 2012 15:32:30 +0200] rev 48439
removed MaSh junk arising from primrec definitions
blanchet [Mon, 23 Jul 2012 15:32:30 +0200] rev 48438
distinguish between recursive and nonrecursive definitions + clean up typedef dependencies in MaSh
blanchet [Mon, 23 Jul 2012 15:32:30 +0200] rev 48437
tuning
blanchet [Mon, 23 Jul 2012 15:32:30 +0200] rev 48436
faster "save" operation
blanchet [Mon, 23 Jul 2012 15:32:30 +0200] rev 48435
include unknown local facts in MaSh
blanchet [Mon, 23 Jul 2012 15:32:30 +0200] rev 48434
ensure all calls to "mash" program are synchronous
blanchet [Mon, 23 Jul 2012 15:32:30 +0200] rev 48433
don't relearn old facts in Isar mode
blanchet [Mon, 23 Jul 2012 15:32:30 +0200] rev 48432
took out CVC3 again -- there seems to be issues with the server version of CVC3 + minor tweaks
haftmann [Mon, 23 Jul 2012 09:28:03 +0200] rev 48431
restrict unqualified imports from Haskell Prelude to a small set of fundamental operations
haftmann [Mon, 23 Jul 2012 09:26:55 +0200] rev 48430
more correct import
wenzelm [Sun, 22 Jul 2012 23:36:11 +0200] rev 48429
merged
haftmann [Sun, 22 Jul 2012 10:00:51 +0200] rev 48428
NEWS
haftmann [Sun, 22 Jul 2012 09:56:34 +0200] rev 48427
library theories for debugging and parallel computing using code generation towards Isabelle/ML
haftmann [Sat, 21 Jul 2012 20:01:16 +0200] rev 48426
also consider current working directory (cf. 3a5a5a992519)
wenzelm [Sun, 22 Jul 2012 23:31:57 +0200] rev 48425
parallel scheduling of jobs;
misc tuning;
wenzelm [Sun, 22 Jul 2012 21:59:14 +0200] rev 48424
tuned;
wenzelm [Sun, 22 Jul 2012 12:26:41 +0200] rev 48423
maintain set of source digests, including relevant parts of session entry;
wenzelm [Sun, 22 Jul 2012 00:00:22 +0200] rev 48422
determine source dependencies, relatively to preloaded theories;
tuned signature;
wenzelm [Sat, 21 Jul 2012 22:13:50 +0200] rev 48421
propagate defined options;
misc tuning;
wenzelm [Sat, 21 Jul 2012 21:16:08 +0200] rev 48420
disallow quotes in path specifications -- extra paranoia;
wenzelm [Sat, 21 Jul 2012 17:49:22 +0200] rev 48419
save image for inner nodes only;
misc tuning and simplification;
wenzelm [Sat, 21 Jul 2012 16:41:55 +0200] rev 48418
some actual build function on ML side;
further imitation of "usedir" shell script;
wenzelm [Sat, 21 Jul 2012 12:57:31 +0200] rev 48417
tuned -- no dependency on exit function;
wenzelm [Sat, 21 Jul 2012 12:42:28 +0200] rev 48416
more ML_System operations;
bulwahn [Sat, 21 Jul 2012 10:55:42 +0200] rev 48415
restricting Quickcheck_Examples' root file to one basic theory to see if the system error on isatest still occurs
bulwahn [Sat, 21 Jul 2012 10:53:26 +0200] rev 48414
handling partiality in the case where the equality optimisation is applied
wenzelm [Fri, 20 Jul 2012 23:38:15 +0200] rev 48413
merged
wenzelm [Fri, 20 Jul 2012 23:37:54 +0200] rev 48412
updated File.find_files;
wenzelm [Fri, 20 Jul 2012 23:16:54 +0200] rev 48411
more abstract file system operations in Scala, corresponding to ML version;
wenzelm [Fri, 20 Jul 2012 22:39:59 +0200] rev 48410
eliminated obsolete session_manager.scala;
wenzelm [Fri, 20 Jul 2012 22:29:25 +0200] rev 48409
more explicit java.io.{File => JFile};
blanchet [Fri, 20 Jul 2012 22:43:51 +0200] rev 48408
tune Mesh filter
blanchet [Fri, 20 Jul 2012 22:19:46 +0200] rev 48407
faster maximal node computation
blanchet [Fri, 20 Jul 2012 22:19:46 +0200] rev 48406
honor suggested MaSh weights
blanchet [Fri, 20 Jul 2012 22:19:46 +0200] rev 48405
use CVC3 and Yices by default if they are available and there are enough cores
blanchet [Fri, 20 Jul 2012 22:19:46 +0200] rev 48404
relearn ATP proofs
blanchet [Fri, 20 Jul 2012 22:19:46 +0200] rev 48403
don't store fresh names in fact graph, since these cannot be the parents of any other facts
blanchet [Fri, 20 Jul 2012 22:19:46 +0200] rev 48402
added MaSh to news
blanchet [Fri, 20 Jul 2012 22:19:46 +0200] rev 48401
cached ancestor computation
blanchet [Fri, 20 Jul 2012 22:19:46 +0200] rev 48400
minimal maxes + tuning
blanchet [Fri, 20 Jul 2012 22:19:46 +0200] rev 48399
learn from SMT proofs when they can be minimized by Metis
blanchet [Fri, 20 Jul 2012 22:19:46 +0200] rev 48398
clean up interesting constants a bit
blanchet [Fri, 20 Jul 2012 22:19:46 +0200] rev 48397
convenience
blanchet [Fri, 20 Jul 2012 22:19:46 +0200] rev 48396
name tuning
blanchet [Fri, 20 Jul 2012 22:19:46 +0200] rev 48395
learning should honor the fact override and the chained facts
blanchet [Fri, 20 Jul 2012 22:19:46 +0200] rev 48394
fixed various issues with MaSh's file handling + tune output + generate local facts again + handle nameless facts gracefully
blanchet [Fri, 20 Jul 2012 22:19:46 +0200] rev 48393
MaSh docs