src/HOL/Tools/Function/partial_function.ML
Mon, 11 Sep 2017 18:36:13 +0200 wenzelm clarified signature: proper result;
less more (0) -30 -10 -1 tip