src/HOL/Tools/Function/function_lib.ML
Thu, 07 Jan 2016 15:53:39 +0100 wenzelm more uniform treatment of package internals;
Sun, 06 Sep 2015 21:55:13 +0200 wenzelm do not expose low-level "_def" facts of 'function' definitions, to avoid potential confusion with the situation of plain 'definition';
Mon, 01 Jun 2015 13:35:16 +0200 wenzelm clarified context;
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;
Wed, 04 Mar 2015 19:53:18 +0100 wenzelm tuned signature -- prefer qualified names;
less more (0) -30 -10 -7 tip