src/HOL/Tools/BNF/bnf_lfp_rec_sugar.ML
Wed, 14 Jul 2021 10:02:43 +0200 blanchet correctly translate constructor argument in 'primrec'
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;
Fri, 09 Aug 2019 17:14:49 +0200 wenzelm formal position for PThm nodes;
Tue, 26 Mar 2019 22:13:36 +0100 wenzelm more informative Spec_Rules.Equational, notably primrec argument types;
Fri, 04 Jan 2019 23:22:53 +0100 wenzelm isabelle update -u control_cartouches;
Sun, 28 Jan 2018 19:28:52 +0100 wenzelm clarified take/drop/chop prefix/suffix;
Thu, 20 Jul 2017 16:28:43 +0100 blanchet strengthened tactic
Wed, 19 Jul 2017 22:56:16 +0100 blanchet strengthened tactic (for 'fun' BNF)
Sun, 02 Jul 2017 20:13:38 +0200 haftmann proper concept of code declaration wrt. atomicity and Isar declarations
Fri, 30 Dec 2016 15:40:35 +0100 blanchet more uniform errors in '(prim)(co)rec(ursive)' variants
Wed, 28 Dec 2016 17:22:16 +0100 blanchet print constants in 'primrec', 'primcorec(ursive)', 'corec(ursive)', like in 'definition' and 'fun(ction)'
Tue, 23 Aug 2016 15:19:32 +0200 traytel tuned signature
Mon, 06 Jun 2016 21:28:46 +0200 haftmann explicit tagging of code equations de-baroquifies interface
Mon, 30 May 2016 20:58:16 +0200 wenzelm tuned;
Thu, 28 Apr 2016 09:43:11 +0200 wenzelm support 'assumes' in specifications, e.g. 'definition', 'inductive';
Wed, 02 Mar 2016 10:02:12 +0100 traytel respect qualification when noting theorems in prim(co)rec
Wed, 17 Feb 2016 11:54:34 +0100 blanchet allow predicator instead of map function in 'primrec'
Tue, 16 Feb 2016 17:01:40 +0100 blanchet avoid duplicate theorems in 'primrec's result when invoked programmatically
Tue, 01 Dec 2015 13:07:40 +0100 blanchet tuned whitespace
Fri, 25 Sep 2015 23:01:31 +0200 traytel more canonical context threading
Thu, 16 Jul 2015 12:23:22 +0200 traytel {r,e,d,f}tac with proper context in BNF
Fri, 10 Apr 2015 23:58:07 +0200 wenzelm make SML/NJ more happy;
Fri, 10 Apr 2015 19:05:00 +0200 blanchet have 'primrec' return definitions
Fri, 10 Apr 2015 18:23:01 +0200 blanchet renamed ML funs
Mon, 06 Apr 2015 17:06:48 +0200 wenzelm @{command_spec} is superseded by @{command_keyword};
Tue, 31 Mar 2015 00:11:54 +0200 wenzelm tuned signature;
Tue, 10 Mar 2015 20:53:16 +0100 blanchet tuning
Thu, 05 Mar 2015 11:57:34 +0100 blanchet tuned new primrec messages
Sun, 11 Jan 2015 21:06:47 +0100 wenzelm tuned warnings: observe Context_Position.is_visible;
Mon, 05 Jan 2015 21:24:14 +0100 blanchet generate [code] only with 'code' plugin enabled
Mon, 05 Jan 2015 10:09:42 +0100 blanchet added plugins syntax to prim(co)rec
Mon, 05 Jan 2015 09:54:41 +0100 blanchet tuning
Fri, 19 Dec 2014 14:06:13 +0100 desharna Add plugin to generate transfer theorem for primrec and primcorec
Wed, 26 Nov 2014 20:05:34 +0100 wenzelm renamed "pairself" to "apply2", in accordance to @{apply 2};
Thu, 13 Nov 2014 14:14:13 +0100 traytel do not introduce consts too early unnecessarily
Wed, 08 Oct 2014 17:09:07 +0200 wenzelm added parameterized ML antiquotations @{map N}, @{fold N}, @{fold_map N}, @{split_list N};
Fri, 19 Sep 2014 13:27:04 +0200 blanchet made new 'primrec' bootstrapping-capable
Fri, 19 Sep 2014 13:27:04 +0200 blanchet tuning
Fri, 19 Sep 2014 13:27:04 +0200 blanchet tuning
Thu, 11 Sep 2014 19:45:42 +0200 blanchet tuning terminology
Thu, 11 Sep 2014 18:54:36 +0200 blanchet tuning
Thu, 11 Sep 2014 18:54:36 +0200 blanchet fixed situation in 'primrec' when recursive calls are apparently nested, e.g. 'f (f x y) y', with the recursion in 'y'
Thu, 11 Sep 2014 18:54:36 +0200 blanchet tuning
Thu, 11 Sep 2014 18:54:36 +0200 blanchet fixed situation in 'primrec' whereby the original value of a constructor argument of nested type was not translated correctly to a 'map fst'
Tue, 09 Sep 2014 20:51:36 +0200 blanchet preserve case names in '(co)induct' theorems generated by prim(co)rec'
Tue, 09 Sep 2014 20:51:36 +0200 blanchet tuning
Mon, 08 Sep 2014 14:03:40 +0200 blanchet export useful functions for users of (co)recursors
Mon, 08 Sep 2014 14:03:08 +0200 blanchet wildcards in plugins
Mon, 08 Sep 2014 14:03:01 +0200 blanchet extended 'datatype_compat' to generate the expected, old-style recursor in the presence of recursion through functions
Fri, 05 Sep 2014 00:41:01 +0200 blanchet fixed infinite loops in 'register' functions + more uniform API
Mon, 01 Sep 2014 16:17:46 +0200 blanchet renamed modules defining old datatypes, as a step towards having 'datatype_new' take 'datatype's place
Thu, 24 Jul 2014 00:24:00 +0200 blanchet repaired named derivations
Mon, 14 Jul 2014 01:22:59 +0200 panny catch "not found" case
Mon, 07 Jul 2014 16:06:46 +0200 desharna add helper function map_prod
Fri, 27 Jun 2014 10:11:44 +0200 blanchet compile
Fri, 27 Jun 2014 10:11:44 +0200 blanchet tuned variable names
Tue, 13 May 2014 11:10:22 +0200 blanchet tuning
Mon, 05 May 2014 08:30:38 +0200 blanchet note correct induction schemes in 'primrec' (for N2M)
Wed, 23 Apr 2014 10:23:27 +0200 blanchet localize new size function generation code
less more (0) -60 tip