src/HOL/Tools/Function/function_lib.ML
Fri, 15 Oct 2021 22:00:28 +0200 wenzelm revert bbfed17243af, breaks HOL-Proofs extraction;
Fri, 15 Oct 2021 20:54:13 +0200 wenzelm proper context for Goal.prove_internal;
Fri, 15 Oct 2021 19:25:31 +0200 wenzelm discontinued Term.dest_abs / Logic.dest_all, which are officially superseded by Variable.dest_abs etc., but there are also Term.dest_abs_global to recover existing tools easily;
Fri, 04 Jan 2019 23:22:53 +0100 wenzelm isabelle update -u control_cartouches;
Wed, 06 Dec 2017 20:43:09 +0100 wenzelm prefer control symbol antiquotations;
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;
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) -14 tip