src/HOL/Tools/Function/partial_function.ML
Mon, 11 Sep 2017 18:36:13 +0200 wenzelm clarified signature: proper result;
Sat, 11 Jun 2016 16:41:11 +0200 wenzelm clarified syntax;
Mon, 30 May 2016 14:15:44 +0200 wenzelm allow 'for' fixes for multi_specs;
Fri, 27 May 2016 20:23:55 +0200 wenzelm tuned proofs, to allow unfold_abs_def;
Thu, 28 Apr 2016 09:43:11 +0200 wenzelm support 'assumes' in specifications, e.g. 'definition', 'inductive';
Mon, 18 Apr 2016 11:02:07 +0200 wenzelm avoid clash with function called "x";
Sun, 17 Apr 2016 22:10:09 +0200 wenzelm clarified bindings;
Sun, 17 Apr 2016 20:11:02 +0200 wenzelm clarified signature;
Sun, 17 Apr 2016 12:40:48 +0200 wenzelm clarified reported positions;
Sun, 17 Apr 2016 12:26:22 +0200 wenzelm operate on proper binding;
Wed, 13 Apr 2016 18:01:05 +0200 wenzelm eliminated "xname" and variants;
Thu, 07 Jan 2016 15:53:39 +0100 wenzelm more uniform treatment of package internals;
Mon, 14 Dec 2015 11:20:31 +0100 wenzelm tuned signature;
Sun, 13 Dec 2015 21:56:15 +0100 wenzelm more general types Proof.method / context_tactic;
Tue, 13 Oct 2015 09:21:15 +0200 haftmann prod_case as canonical name for product type eliminator
less more (0) -15 tip