src/HOL/Tools/BNF/bnf_def_tactics.ML
Mon, 18 Dec 2017 11:56:12 +0100 traytel removed debug output
Sun, 17 Dec 2017 08:42:59 +0100 traytel made tactics more robust
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;
Mon, 14 Mar 2016 12:31:05 +0100 blanchet strengthened tactics
Wed, 17 Feb 2016 15:18:06 +0100 traytel derive transfer rule for predicator
Tue, 16 Feb 2016 22:28:19 +0100 traytel make predicator a first-class bnf citizen
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
Thu, 24 Sep 2015 12:28:15 +0200 traytel congruence rules for the relator
Sat, 18 Jul 2015 21:44:18 +0200 wenzelm prefer tactics with explicit context;
Sat, 18 Jul 2015 20:47:08 +0200 wenzelm prefer tactics with explicit context;
Thu, 16 Jul 2015 12:23:22 +0200 traytel {r,e,d,f}tac with proper context in BNF
Tue, 10 Feb 2015 14:48:26 +0100 wenzelm proper context for resolve_tac, eresolve_tac, dresolve_tac, forward_tac etc.;
Thu, 25 Sep 2014 16:35:53 +0200 desharna generate 'rec_transfer' for datatypes
Mon, 01 Sep 2014 13:53:34 +0200 desharna generate 'set_transfer' for BNFs
Mon, 01 Sep 2014 13:23:39 +0200 desharna generate 'rel_transfer' for BNFs
Mon, 18 Aug 2014 14:09:09 +0200 desharna generate 'inj_map_strong' for BNFs
Mon, 18 Aug 2014 13:46:22 +0200 desharna renamed 'rel_mono_strong' to 'rel_mono_strong0'
Thu, 14 Aug 2014 13:20:54 +0200 desharna generate 'rel_map' theorem for BNFs
Fri, 25 Jul 2014 11:26:10 +0200 blanchet tuning
Thu, 08 May 2014 11:52:44 +0200 desharna generate 'map_ident' theorem for BNFs
Wed, 23 Apr 2014 10:23:26 +0200 blanchet added 'inj_map' as auxiliary BNF theorem
Fri, 07 Mar 2014 22:30:58 +0100 wenzelm more antiquotations;
Thu, 06 Mar 2014 15:40:33 +0100 blanchet renamed 'fun_rel' to 'rel_fun'
Fri, 21 Feb 2014 00:09:56 +0100 blanchet adapted to renaming of datatype 'cases' and 'recs' to 'case' and 'rec'
Wed, 12 Feb 2014 08:35:57 +0100 blanchet renamed '{prod,sum,bool,unit}_case' to 'case_...'
Fri, 31 Jan 2014 10:02:36 +0100 traytel less hermetic tactics
Wed, 29 Jan 2014 16:35:05 +0100 traytel made tactic more robust
Mon, 20 Jan 2014 18:24:56 +0100 blanchet tuned names
Mon, 20 Jan 2014 18:24:56 +0100 blanchet adjusted comments
Mon, 20 Jan 2014 18:24:56 +0100 blanchet avoid nested 'Tools' directories
less more (0) tip