src/HOL/Tools/Function/function_lib.ML
Mon, 18 Apr 2016 14:30:24 +0200 wenzelm clarified bindings;
less more (0) -30 -10 -1 tip