Summary
- merged
- clarified data representation: prefer explicit type Thm_Name;
- more operations, following Isabelle/ML;
- clarified signature: more explicit operations;
- clarified treatment of Thm_Name.T (again, see also 8a9588ffc133);
- clarified operations, including exceptions;
- tuned: more direct Isabelle/ML;
- clarified modules;
- more accurate thm "name_hint", using Thm_Name.T;
- more operationsd;
- tuned;
- more robust: prefer synchronous compression (usually <= 1ms, sometimes 1..5ms);
- clarified signature;
- clarified output, following Consumer_Thread.failure;
- more informative exception output, with optional trace;
- more accurate output of Thm_Name.T wrt. facts name space;
- clarified signature: more operations;
- tuned structure;
- tuned;
- more accurate Thm_Name.T for PThm / Thm.name_derivation / Thm.derivation_name;
- clarified signature: prefer explicit operation;
- clarified signature;
- tuned: prefer Thm_Name operations;
- tuned;
- prefer dynamic position from command transaction;
- tuned signature;
- clarified signature: more explicit preprocessing;
- clarified signature: separate formal context from exported theory_name;
- tuned signature: just one ZThm is sufficient;