src/HOL/Tools/Function/function_lib.ML
Fri, 21 Mar 2014 20:33:56 +0100 wenzelm more qualified names;
Tue, 31 Dec 2013 14:29:16 +0100 wenzelm proper context for norm_hhf and derived operations;
less more (0) -10 -2 tip