src/Pure/Syntax/syntax_trans.ML
Fri, 06 Dec 2024 22:40:43 +0100 wenzelm tuned signature;
Fri, 06 Dec 2024 20:26:33 +0100 wenzelm clarified renaming of bounds, using Syntax_Trans.variant_bounds: avoid structures and fixed variables with syntax;
Fri, 06 Dec 2024 15:20:43 +0100 wenzelm tuned signature;
Fri, 06 Dec 2024 13:33:25 +0100 wenzelm 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");
less more (0) -30 -10 -4 tip