src/HOL/Tools/Predicate_Compile/code_prolog.ML
Mon, 22 Feb 2021 15:24:04 +0100 wenzelm clarified signature: always trim_line of Process_Result.out/err, uniformly in ML and Scala;
less more (0) -100 -30 -10 -1 tip