| Fri, 19 Oct 2012 12:08:13 +0200 | wenzelm | clarified Future.map (again): finished value is mapped in-place, which saves task structures and changes error behaviour slightly (tolerance against canceled group of old value etc.); | changeset | files |
| Thu, 18 Oct 2012 20:59:46 +0200 | wenzelm | back to polyml-5.4.1 (cf. b3110dec1a32) -- no cause of spurious interrupts; | changeset | files |
| Thu, 18 Oct 2012 20:45:15 +0200 | wenzelm | merged | changeset | files |
| Thu, 18 Oct 2012 20:00:45 +0200 | wenzelm | back to parallel HOL-BNF-Examples, which seems to have suffered from Future.map on canceled persistent futures; | changeset | files |
| Thu, 18 Oct 2012 19:58:30 +0200 | wenzelm | more basic Goal.reset_futures as snapshot of implicit state; | changeset | files |
| Thu, 18 Oct 2012 19:12:58 +0200 | wenzelm | tuned proof; | changeset | files |