src/HOL/Tools/BNF/bnf_comp_tactics.ML
Wed, 17 Feb 2016 21:51:56 +0100 haftmann prefer abbreviations for compound operators INFIMUM and SUPREMUM
Tue, 16 Feb 2016 22:28:19 +0100 traytel make predicator a first-class bnf citizen
Tue, 01 Dec 2015 13:07:40 +0100 blanchet tuned whitespace
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, 04 Sep 2014 09:02:43 +0200 blanchet renamed internal constant
Fri, 07 Mar 2014 22:30:58 +0100 wenzelm more antiquotations;
Thu, 06 Mar 2014 12:17:26 +0100 traytel more careful simplification of sets (cf. abf91ebd0820)---yields smaller terms
Tue, 04 Mar 2014 18:57:17 +0100 blanchet simplify sets in BNF composition
Tue, 04 Mar 2014 18:57:17 +0100 blanchet tuning
Mon, 03 Mar 2014 12:48:19 +0100 blanchet optimize cardinal bounds involving natLeq (omega)
Mon, 24 Feb 2014 10:16:10 +0100 traytel clarified interaction with dead variables in the composition of BNFs
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