src/HOL/Tools/BNF/bnf_gfp_rec_sugar.ML
Thu, 01 May 2014 14:07:27 +0200 panny use qualified name (was interpreted as a catch-all variable name)
Thu, 01 May 2014 14:05:29 +0200 panny add additional check to avoid selector formula right-hand side consisting of a nullary constructor getting interpreted as a discriminator formula
Sat, 22 Mar 2014 18:19:57 +0100 wenzelm more antiquotations;
Sat, 15 Mar 2014 01:36:38 +0100 panny add error messages for invalid inputs
Fri, 07 Mar 2014 14:21:15 +0100 blanchet use balanced tuples in 'primcorec'
Fri, 07 Mar 2014 01:02:21 +0100 blanchet balance tuples that represent curried functions
Mon, 03 Mar 2014 12:48:20 +0100 blanchet removed (co)iterators from documentation
Mon, 03 Mar 2014 12:48:20 +0100 blanchet avoid duplicate 'disc_iff' theorems
Mon, 03 Mar 2014 12:48:20 +0100 blanchet rationalized internals
Mon, 03 Mar 2014 12:48:20 +0100 blanchet rationalize internals
Mon, 03 Mar 2014 12:48:20 +0100 blanchet make 'diff_iff' a simp rule if available
Mon, 03 Mar 2014 12:48:20 +0100 blanchet less aggressive resolving
Thu, 27 Feb 2014 13:04:57 +0100 blanchet correct most general type for mutual recursion when several identical types are involved
Tue, 18 Feb 2014 23:08:59 +0100 blanchet prepare two-stage 'primrec' setup
Mon, 17 Feb 2014 22:54:38 +0100 blanchet simplified data structure by reducing the incidence of clumsy indices
Mon, 17 Feb 2014 18:18:27 +0100 blanchet tuning
Mon, 17 Feb 2014 13:31:42 +0100 blanchet tuning: moved code where it belongs
Mon, 17 Feb 2014 13:31:41 +0100 blanchet tuning
Fri, 14 Feb 2014 15:03:24 +0100 blanchet allow different functions to recurse on the same type, like in the old package
Fri, 14 Feb 2014 07:53:45 +0100 blanchet added 'Spec_Rules' for 'primcorec'
Wed, 12 Feb 2014 08:35:57 +0100 blanchet renamed '{prod,sum,bool,unit}_case' to 'case_...'
Wed, 12 Feb 2014 08:35:56 +0100 blanchet tuning
Thu, 06 Feb 2014 00:43:57 +0100 blanchet don't waste time with old-style 'case's that don't have the required theorems
Thu, 06 Feb 2014 00:24:02 +0100 blanchet expand 'split' in direct corecursion as well
Thu, 06 Feb 2014 00:03:12 +0100 blanchet tuning
Wed, 05 Feb 2014 23:30:02 +0100 blanchet adapted tactic to correctly handle 'if ... then ...' and 'case ...' under lambdas
Wed, 05 Feb 2014 17:59:12 +0100 blanchet properly massage 'if's / 'case's etc. under lambdas
Tue, 21 Jan 2014 16:56:34 +0100 blanchet made SML/NJ happier
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