src/HOL/Tools/Function/function_common.ML
Tue, 04 Jun 2019 20:49:33 +0200 wenzelm tuned;
less more (0) -30 -10 -1 tip