src/HOL/Tools/BNF/bnf_def.ML
Fri, 04 Jan 2019 23:22:53 +0100 wenzelm isabelle update -u control_cartouches;
Sun, 17 Dec 2017 08:42:59 +0100 traytel made tactics more robust
Tue, 11 Jul 2017 21:36:42 +0200 traytel store the unfolded definitions of the lifted bnf constants under "_def" name
Tue, 27 Jun 2017 00:07:34 +0200 blanchet more error checking
Wed, 21 Dec 2016 12:49:15 +0100 blanchet generalized ML function (towards nonuniform datatypes)
Tue, 01 Nov 2016 16:04:35 +0100 traytel tuned signature
Tue, 13 Sep 2016 16:23:12 +0200 blanchet union associates to the left
Mon, 12 Sep 2016 13:35:29 +0200 blanchet prove 'set' property backward
Thu, 18 Aug 2016 11:10:07 +0200 traytel derive pred_mono property for BNFs
Tue, 05 Jul 2016 22:47:48 +0200 wenzelm more antiquotations;
Fri, 27 May 2016 20:23:55 +0200 wenzelm tuned proofs, to allow unfold_abs_def;
Mon, 18 Apr 2016 14:26:21 +0200 wenzelm tuned;
Tue, 01 Mar 2016 13:11:56 +0100 blanchet generalized ML function
Fri, 26 Feb 2016 15:49:35 +0100 blanchet generalized ML function
Wed, 17 Feb 2016 15:18:06 +0100 traytel derive transfer rule for predicator
Wed, 17 Feb 2016 11:54:34 +0100 blanchet allow predicator instead of map function in 'primrec'
Tue, 16 Feb 2016 22:28:19 +0100 traytel make predicator a first-class bnf citizen
Thu, 07 Jan 2016 15:53:39 +0100 wenzelm more uniform treatment of package internals;
Sun, 13 Dec 2015 21:56:15 +0100 wenzelm more general types Proof.method / context_tactic;
Tue, 01 Dec 2015 13:07:40 +0100 blanchet tuned whitespace
Tue, 13 Oct 2015 09:21:15 +0200 haftmann prod_case as canonical name for product type eliminator
Tue, 06 Oct 2015 12:01:07 +0200 traytel collect the names from goals in favor of fragile exports
Thu, 01 Oct 2015 17:32:07 +0200 blanchet export '_cmd' functions
Fri, 25 Sep 2015 23:01:31 +0200 traytel more canonical context threading
Thu, 24 Sep 2015 12:28:15 +0200 traytel congruence rules for the relator
Thu, 24 Sep 2015 12:21:19 +0200 traytel conceal only the definitional theorems of map, set, rel (and not the actual constants)
Thu, 24 Sep 2015 12:21:19 +0200 traytel more useful properties of the relators
Fri, 04 Sep 2015 21:40:59 +0200 wenzelm close derivation *before* splitting conjuncts, like Goal.prove_common (see also 757cad5a3fe9) -- potential improvement of performance;
Thu, 03 Sep 2015 16:41:43 +0200 traytel use open/close_target rather than Local_Theory.restore to get polymorphic definitions;
Sun, 16 Aug 2015 18:19:30 +0200 wenzelm prefer theory_id operations;
Thu, 13 Aug 2015 13:55:52 +0200 wenzelm merged
Thu, 13 Aug 2015 11:05:19 +0200 wenzelm tuned signature, in accordance to sortBy in Scala;
Wed, 12 Aug 2015 20:46:33 +0200 traytel new command for lifting BNF structure over typedefs
Mon, 27 Jul 2015 17:44:55 +0200 wenzelm tuned signature;
Sun, 26 Jul 2015 17:24:54 +0200 wenzelm updated to infer_instantiate;
Fri, 17 Jul 2015 16:13:03 +0200 traytel forgotten selector
Thu, 16 Jul 2015 12:23:22 +0200 traytel {r,e,d,f}tac with proper context in BNF
Tue, 28 Apr 2015 22:57:07 +0200 blanchet allow sorts on dead variables in BNFs
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;
Mon, 30 Mar 2015 22:34:59 +0200 wenzelm support for strictly private name space entries;
Fri, 27 Mar 2015 09:56:34 +0100 blanchet sort BNFs in output
Mon, 16 Mar 2015 23:05:56 +0100 traytel BNF relators preserve reflexivity
Tue, 10 Mar 2015 09:49:17 +0100 blanchet split into subgoals
Fri, 06 Mar 2015 15:58:56 +0100 wenzelm Thm.cterm_of and Thm.ctyp_of operate on local context;
Tue, 03 Mar 2015 19:08:04 +0100 traytel eliminated some clones of Proof_Context.cterm_of
Mon, 05 Jan 2015 10:09:42 +0100 blanchet added plugins syntax to prim(co)rec
Thu, 11 Dec 2014 14:14:39 +0100 traytel note more facts (always)
Wed, 26 Nov 2014 20:05:34 +0100 wenzelm renamed "pairself" to "apply2", in accordance to @{apply 2};
Mon, 03 Nov 2014 14:50:27 +0100 wenzelm eliminated unused int_only flag (see also c12484a27367);
Mon, 13 Oct 2014 19:34:10 +0200 wenzelm clarified load order;
Mon, 13 Oct 2014 18:45:48 +0200 wenzelm Local_Interpretation is superseded by Plugin with formal Plugin_Name management, avoiding undeclared strings;
Wed, 08 Oct 2014 17:09:07 +0200 wenzelm added parameterized ML antiquotations @{map N}, @{fold N}, @{fold_map N}, @{split_list N};
Wed, 24 Sep 2014 16:35:42 +0200 blanchet improved 'bnf' parser
Tue, 16 Sep 2014 19:23:37 +0200 blanchet register 'prod' and 'sum' as datatypes, to allow N2M through them
Mon, 15 Sep 2014 16:14:14 +0200 blanchet set 'mono' attribute on 'rel_mono'
Fri, 05 Sep 2014 00:41:01 +0200 blanchet added 'plugins' option to control which hooks are enabled
Fri, 05 Sep 2014 00:41:01 +0200 blanchet introduced mechanism to filter interpretations
Fri, 05 Sep 2014 00:41:01 +0200 blanchet fixed infinite loops in 'register' functions + more uniform API
Fri, 05 Sep 2014 00:41:01 +0200 blanchet named interpretations
less more (0) -100 -60 tip