src/HOL/Tools/Function/function_common.ML
Thu, 28 Nov 2019 18:13:23 +0100 wenzelm more structural integrity;
Tue, 04 Jun 2019 20:49:33 +0200 wenzelm tuned;
Mon, 03 Jun 2019 23:29:05 +0200 wenzelm tuned;
Mon, 19 Feb 2018 14:49:11 +0100 wenzelm tuned signature;
Sun, 18 Feb 2018 17:57:14 +0100 wenzelm more explicit instantiate_morphism (without checks for typ / term component);
Fri, 16 Feb 2018 21:33:04 +0100 wenzelm trim context of persistent data;
Wed, 06 Dec 2017 20:43:09 +0100 wenzelm prefer control symbol antiquotations;
Wed, 05 Apr 2017 10:26:28 +0200 Lars Hupel store totality fact in function info
Mon, 30 May 2016 20:58:16 +0200 wenzelm tuned;
Thu, 28 Apr 2016 09:43:11 +0200 wenzelm support 'assumes' in specifications, e.g. 'definition', 'inductive';
Mon, 18 Apr 2016 14:26:42 +0200 wenzelm tuned;
Sun, 17 Apr 2016 22:10:09 +0200 wenzelm clarified bindings;
Sun, 17 Apr 2016 20:54:17 +0200 wenzelm prefer binding over base name;
Sun, 17 Apr 2016 16:36:47 +0200 wenzelm removed pointless check (see Type_Infer.object_logic);
Fri, 04 Sep 2015 13:39:20 +0200 wenzelm trim context for persistent storage;
less more (0) -15 tip