src/HOL/Tools/BNF/bnf_tactics.ML
Tue, 05 Jul 2016 22:47:48 +0200 wenzelm more antiquotations;
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
Wed, 04 Mar 2015 19:53:18 +0100 wenzelm tuned signature -- prefer qualified names;
Wed, 26 Nov 2014 20:05:34 +0100 wenzelm renamed "pairself" to "apply2", in accordance to @{apply 2};
Thu, 18 Sep 2014 16:47:40 +0200 blanchet made 'mk_pointfree' work again in local theories
Tue, 16 Sep 2014 19:23:37 +0200 blanchet register 'prod' and 'sum' as datatypes, to allow N2M through them
Sat, 13 Sep 2014 18:08:38 +0200 blanchet imported patch phantoms
Fri, 07 Mar 2014 22:30:58 +0100 wenzelm more antiquotations;
Wed, 26 Feb 2014 10:10:38 +0100 traytel made tactics more robust
Tue, 18 Feb 2014 23:08:57 +0100 blanchet removed deadcode
Wed, 05 Feb 2014 23:30:02 +0100 blanchet adapted tactic to correctly handle 'if ... then ...' and 'case ...' under lambdas
Fri, 31 Jan 2014 10:02:36 +0100 traytel less hermetic tactics
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