src/HOL/Tools/Function/function_lib.ML
Fri, 06 Mar 2015 20:08:45 +0100 wenzelm proper context;
Fri, 06 Mar 2015 15:58:56 +0100 wenzelm Thm.cterm_of and Thm.ctyp_of operate on local context;
Fri, 06 Mar 2015 13:39:34 +0100 wenzelm clarified context;
less more (0) -10 -3 tip