src/Pure/Syntax/syntax_ext.ML
Fri, 13 Dec 2024 23:23:07 +0100 wenzelm minor performance tuning: avoid excessive Library.insert and Symbol.explode operations;
less more (0) -30 -10 -1 tip