Sat, 19 Jan 2013 22:18:35 +0100 | wenzelm | afford parallel proof terms; | changeset | files |
Sat, 19 Jan 2013 22:17:26 +0100 | wenzelm | always close derivation at the bottom of forked proofs (despite increased non-determinism of proof terms) -- improve parallel performance by avoiding dynamic dependency within large Isar proofs, e.g. Slicing/JinjaVM/SemanticsWF.thy in AFP/bf9b14cbc707; | changeset | files |