isabelle: Changelog

wenzelm [Tue, 19 Dec 2023 17:54:55 +0100] rev 79308

more robust: avoid assumption about Context.certificate_theory;

wenzelm [Tue, 19 Dec 2023 17:31:12 +0100] rev 79307

tuned;

wenzelm [Tue, 19 Dec 2023 17:26:30 +0100] rev 79306

clarified pro-forma proof: no zboxes here (partially revert 686b7b14d041);

wenzelm [Tue, 19 Dec 2023 17:07:22 +0100] rev 79305

tuned;

wenzelm [Tue, 19 Dec 2023 15:27:45 +0100] rev 79304

tuned;

wenzelm [Tue, 19 Dec 2023 15:17:04 +0100] rev 79303

more normalization;

wenzelm [Tue, 19 Dec 2023 14:41:28 +0100] rev 79302

less ambitious normalization: term abstractions over terms and proofs, but not proofs over proofs (which may be large);

wenzelm [Tue, 19 Dec 2023 12:44:03 +0100] rev 79301

tuned;

wenzelm [Tue, 19 Dec 2023 12:41:52 +0100] rev 79300

more thorough beta contraction, following Envir.norm_term;

wenzelm [Tue, 19 Dec 2023 12:35:24 +0100] rev 79299

tuned, following Envir.norm_term;

isabelle