src/HOL/Tools/Function/function_lib.ML
Tue, 31 Dec 2013 14:29:16 +0100 wenzelm proper context for norm_hhf and derived operations;
less more (0) -10 -1 tip