src/HOL/Tools/Function/function_lib.ML
Mon, 18 Apr 2016 14:30:24 +0200 wenzelm clarified bindings;
Sun, 17 Apr 2016 22:10:09 +0200 wenzelm clarified bindings;
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;
less more (0) -30 -10 -7 tip