src/HOL/Tools/Function/partial_function.ML
Tue, 21 Jan 2025 19:26:39 +0100 wenzelm misc tuning: prefer specific variants of Thm.dest_comb;
Sat, 20 May 2023 17:18:44 +0200 wenzelm tuned signature;
Thu, 18 May 2023 17:21:29 +0200 wenzelm clarified signature: more explicit types;
Tue, 18 Apr 2023 22:24:48 +0200 wenzelm tuned;
Wed, 20 Oct 2021 18:13:17 +0200 wenzelm discontinued obsolete "val extend = I" for data slots;
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, 10 Sep 2021 14:59:19 +0200 wenzelm clarified signature: more scalable operations;
Mon, 02 Dec 2019 15:04:38 +0100 wenzelm proper spec_rule name via naming/binding/Morphism.binding;
Fri, 29 Nov 2019 20:57:04 +0100 wenzelm more informative spec rules: optional name;
Tue, 04 Jun 2019 20:01:02 +0200 wenzelm tuned;
Tue, 04 Jun 2019 19:51:45 +0200 wenzelm backout 34bc296374ee -- affects the raw_induct rule, e.g. relevant for AFP/Imperative_Insertion_Sort;
Tue, 04 Jun 2019 15:14:19 +0200 wenzelm proper context;
Tue, 26 Mar 2019 22:13:36 +0100 wenzelm more informative Spec_Rules.Equational, notably primrec argument types;
Thu, 21 Feb 2019 09:15:07 +0000 haftmann streamlined specification interfaces
less more (0) -15 tip