src/HOL/Tools/Function/partial_function.ML
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) -30 -10 -7 tip