Changes

Summary

1. more robust: avoid looping Lazy.force due to misinterpreted interrupt;
2. more informative combination_proof, e.g. relevant for proper type inference in HOL.Product_Type (with export_proofs);
3. tuned -- more stable type inference;
4. updated to jdk-11.0.4+11;
5. updated to scala-2.12.10;