wenzelm [Fri, 06 Dec 2024 20:46:24 +0100] rev 81546
NEWS;
wenzelm [Fri, 06 Dec 2024 20:26:33 +0100] rev 81545
clarified renaming of bounds, using Syntax_Trans.variant_bounds: avoid structures and fixed variables with syntax;
wenzelm [Fri, 06 Dec 2024 15:20:43 +0100] rev 81544
tuned signature;
wenzelm [Fri, 06 Dec 2024 13:33:25 +0100] rev 81543
clarified printing of consts: rename apart from all bounds, and thus avoid old Term.declare_free_names with its adhoc policy ("as they are printed");
wenzelm [Tue, 03 Dec 2024 22:46:24 +0100] rev 81542
prefer Term.variant_bounds: bounds vs. frees, no attempt at consts;
wenzelm [Mon, 02 Dec 2024 22:16:29 +0100] rev 81541
more elementary operation Term.variant_bounds: only for bounds vs. frees, no consts, no tfrees;
wenzelm [Mon, 02 Dec 2024 20:35:12 +0100] rev 81540
tuned signature;
wenzelm [Mon, 02 Dec 2024 18:53:45 +0100] rev 81539
clarified modules;
wenzelm [Mon, 02 Dec 2024 14:30:10 +0100] rev 81538
more accurate extern_const: avoid clash with frees;
wenzelm [Mon, 02 Dec 2024 14:08:28 +0100] rev 81537
more direct Proof_Context.lookup_free -- bypass redundancy of Proof_Context.check_const;