Mon, 02 Dec 2019 15:04:38 +0100 | wenzelm | proper spec_rule name via naming/binding/Morphism.binding; | file | diff | annotate |
Fri, 29 Nov 2019 20:57:04 +0100 | wenzelm | more informative spec rules: optional name; | file | diff | annotate |
Tue, 04 Jun 2019 20:01:02 +0200 | wenzelm | tuned; | file | diff | annotate |
Tue, 04 Jun 2019 19:51:45 +0200 | wenzelm | backout 34bc296374ee -- affects the raw_induct rule, e.g. relevant for AFP/Imperative_Insertion_Sort; | file | diff | annotate |
Tue, 04 Jun 2019 15:14:19 +0200 | wenzelm | proper context; | file | diff | annotate |
Tue, 26 Mar 2019 22:13:36 +0100 | wenzelm | more informative Spec_Rules.Equational, notably primrec argument types; | file | diff | annotate |
Thu, 21 Feb 2019 09:15:07 +0000 | haftmann | streamlined specification interfaces | file | diff | annotate |