Sat, 13 Mar 2021 13:44:42 +0100 wenzelm clarified signature;
Sat, 13 Mar 2021 12:45:31 +0100 wenzelm tuned;
Sat, 13 Mar 2021 12:36:24 +0100 wenzelm clarified signature: function_thread is determined in Isabelle/Scala, not Isabelle/ML;
(0) -30000 -10000 -3000 -1000 -300 -100 -30 -10 -3 +3 +10 +30 +100 +300 +1000 +3000 tip