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;
Sun, 07 Feb 2021 22:19:39 +0100 wenzelm more complete solutions (amending 4d36070bdbf4);
Sun, 07 Feb 2021 21:25:21 +0100 wenzelm more robust: accommodate output lines produced by Scala "bash_process";
less more (0) -100 -30 -10 -3 tip