src/Pure/Tools/doc.scala
Wed, 25 Jun 2025 12:37:43 +0200 wenzelm tuned signature;
Wed, 25 Jun 2025 12:29:04 +0200 wenzelm clarified signature;
Wed, 25 Jun 2025 12:08:12 +0200 wenzelm clarified signature: more accurate ML_Settings;
less more (0) -30 -10 -3 tip