Thu, 12 Jan 2023 16:01:49 +0100 wenzelm more explicit latex markup;
Wed, 11 Jan 2023 15:00:06 +0100 wenzelm follow recent changes of Sledgehammer defaults, as 0a46b3dbd5ad exposes a hint in the source text;
(0) -30000 -10000 -3000 -1000 -300 -100 -30 -10 -2 +2 +10 +30 +100 +300 +1000 +3000 tip