tuned;

tuned;

clarified pattern matching;

misc tuning;

misc tuning and clarification;

tuned;

clarified exceptions and messages: use "error" only for user-errors, not system failures;

minor performance tuning: more elementary operations;

minor performance tuning;

clarified inst_type: more direct Thm.instantiate_frees;

more direct Thm.free: avoid re-certification;

clarified signature: more explicit types;

tuned names;

tuned names;

tuned signature;

tuned;

tuned signature;

clarified signature: more standard Isabelle/ML;

clarified signature;

more robust import_file path: proper master_directory; support for compressed proofs.zst (e.g. via "zstd -8");

tuned signature: more operations;

unused;

tuned signature, following Isabelle/Scala;

clarified signature, following Isabelle/Scala;

clarified pattern via antiquotations;

misc tuning and clarification;

tuned;

clarified make_type: proper make_name;