src/Pure/Syntax/syntax.ML
Fri, 25 Apr 2025 11:22:25 +0200 wenzelm more scalable: discontinue odd shortcuts from 6b3739fee456, which produce bulky strings internally;
Mon, 27 Jan 2025 18:32:18 +0100 wenzelm more operations;
less more (0) -300 -100 -30 -10 -2 tip