src/HOL/Tools/inductive_codegen.ML
Mon, 17 Oct 2011 10:19:01 +0200 bulwahn moving some common functions from quickcheck to the more HOL-specific quickcheck_common; renamed inductive_SML's configurations to more canonical names; adds automatically left and right hand sides of equations as evaluation terms
Wed, 17 Aug 2011 18:05:31 +0200 wenzelm modernized signature of Term.absfree/absdummy;
Wed, 10 Aug 2011 20:53:43 +0200 wenzelm old term operations are legacy;
Mon, 08 Aug 2011 17:23:15 +0200 wenzelm misc tuning -- eliminated old-fashioned rep_thm;
Mon, 18 Jul 2011 10:34:21 +0200 bulwahn changed every tester to have a configuration in quickcheck; enabling parallel testing of different testers in quickcheck
Mon, 18 Jul 2011 10:34:21 +0200 bulwahn removing generator registration
Fri, 01 Jul 2011 15:16:03 +0200 wenzelm proper @{binding} antiquotations (relevant for formal references);
Thu, 09 Jun 2011 16:34:49 +0200 wenzelm discontinued Name.variant to emphasize that this is old-style / indirect;
Mon, 02 May 2011 16:33:21 +0200 wenzelm added Attrib.setup_config_XXX conveniences, with implicit setup of the background theory;
Wed, 20 Apr 2011 16:49:52 +0200 wenzelm standardized some ML aliases;
Wed, 20 Apr 2011 16:18:47 +0200 wenzelm avoid Display.string_of_thm_without_context;
Wed, 20 Apr 2011 15:55:34 +0200 wenzelm eliminated global references / critical sections via context data;
Tue, 19 Apr 2011 23:57:28 +0200 wenzelm eliminated Codegen.mode in favour of explicit argument;
Sat, 16 Apr 2011 16:15:37 +0200 wenzelm modernized structure Proof_Context;
Wed, 30 Mar 2011 09:44:16 +0200 bulwahn generalizing compilation scheme of quickcheck generators to multiple arguments; changing random and exhaustive tester to use one code invocation for polymorphic instances with multiple cardinalities
Thu, 24 Mar 2011 16:56:19 +0100 wenzelm added Term.is_open and Term.is_dependent convenience, to cover common situations of loose bounds;
Fri, 18 Mar 2011 18:19:42 +0100 bulwahn passing a term with free variables to the quickcheck tester functions instead of an lambda expression because this is more natural with passing further evaluation terms; added output of evaluation terms; added evaluation of terms in the exhaustive testing
Fri, 18 Mar 2011 18:19:42 +0100 bulwahn extending the test data generators to take the evaluation terms as arguments
Thu, 27 Jan 2011 16:24:29 +0100 wenzelm CRITICAL markup for critical poking with unsynchronized references;
Mon, 10 Jan 2011 15:19:48 +0100 wenzelm standardized split_last/last_elem towards List.last;
Sat, 08 Jan 2011 17:14:48 +0100 wenzelm misc tuning and comments based on review of Theory_Data, Proof_Data, Generic_Data usage;
Fri, 07 Jan 2011 18:07:27 +0100 wenzelm do not open Codegen;
Fri, 03 Dec 2010 08:40:47 +0100 bulwahn moving iteration of tests to the testers in quickcheck
Mon, 25 Oct 2010 21:06:56 +0200 wenzelm renamed Output.priority to Output.urgent_message to emphasize its special role more clearly;
Thu, 09 Sep 2010 17:23:03 +0200 bulwahn removing report from the arguments of the quickcheck functions and refering to it by picking it from the context
Thu, 09 Sep 2010 16:43:57 +0200 bulwahn changing the container for the quickcheck options to a generic data
Sat, 28 Aug 2010 16:14:32 +0200 haftmann formerly unnamed infix equality now named HOL.eq
Wed, 11 Aug 2010 15:17:13 +0200 wenzelm use Pretty.enum convenience;
Thu, 01 Jul 2010 16:54:42 +0200 haftmann qualified constants Set.member and Set.Collect
Thu, 24 Jun 2010 14:19:08 +0200 wenzelm avoid equality on abstract type Pretty.T;
Thu, 10 Jun 2010 12:24:02 +0200 haftmann moved inductive_codegen to place where product type is available; tuned structure name
Sun, 30 May 2010 21:34:19 +0200 wenzelm replaced ML_Lex.read_antiq by more concise ML_Lex.read, which includes full read/report with explicit position information;
Mon, 17 May 2010 23:54:15 +0200 wenzelm prefer structure Keyword, Parse, Parse_Spec, Outer_Syntax;
Wed, 05 May 2010 18:25:34 +0200 haftmann farewell to old-style mem infixes -- type inference in situations with mem_int and mem_string should provide enough information to resolve the type of (op =)
Mon, 03 May 2010 14:25:56 +0200 wenzelm renamed ProofContext.init to ProofContext.init_global to emphasize that this is not the real thing;
Sun, 28 Mar 2010 16:59:06 +0200 wenzelm static defaults for configuration options;
Sun, 28 Mar 2010 15:13:19 +0200 wenzelm use regular Attrib.config instead of low-level Config.declare/Attrib.register_config;
Fri, 26 Feb 2010 09:49:00 +0100 bulwahn merged
Thu, 25 Feb 2010 09:28:01 +0100 bulwahn added basic reporting of test cases to quickcheck
Thu, 25 Feb 2010 22:32:09 +0100 wenzelm more antiquotations;
Sun, 07 Feb 2010 19:33:34 +0100 wenzelm renamed old-style Drule.standard to Drule.export_without_context, to emphasize that this is in no way a standard operation;
Fri, 22 Jan 2010 16:56:51 +0100 haftmann HOLogic.strip_psplits: types are ordered after syntactic appearance, not after corresponding de-Bruin index (closer correspondence to similar strip operations)
Fri, 27 Nov 2009 08:41:10 +0100 haftmann renamed former datatype.ML to datatype_data.ML; datatype.ML provides uniform view on datatype.ML and datatype_rep_proofs.ML
Thu, 19 Nov 2009 16:07:53 +0100 berghofe Added new counterexample generator SML_inductive for goals involving
Sun, 08 Nov 2009 18:43:42 +0100 wenzelm adapted Theory_Data;
Thu, 29 Oct 2009 23:49:55 +0100 wenzelm eliminated some old folds;
Thu, 29 Oct 2009 17:58:26 +0100 wenzelm standardized filter/filter_out;
Tue, 27 Oct 2009 22:55:27 +0100 wenzelm Datatype.read_typ: standard argument order;
Thu, 22 Oct 2009 13:48:06 +0200 haftmann map_range (and map_index) combinator
Wed, 21 Oct 2009 12:12:21 +0200 haftmann merged
Wed, 21 Oct 2009 12:09:37 +0200 haftmann curried inter as canonical list operation (beware of argument order)
Wed, 21 Oct 2009 12:02:56 +0200 haftmann curried union as canonical list operation
Wed, 21 Oct 2009 08:14:38 +0200 haftmann dropped redundant gen_ prefix
Tue, 20 Oct 2009 16:13:01 +0200 haftmann replaced old_style infixes eq_set, subset, union, inter and variants by generic versions
Sat, 17 Oct 2009 00:52:37 +0200 wenzelm explicitly qualify Drule.standard;
Thu, 15 Oct 2009 23:28:10 +0200 wenzelm replaced String.concat by implode;
Thu, 30 Jul 2009 15:20:57 +0200 haftmann path-sensitive tuple combinators carry a "p"(ath) prefix; combinators for standard right-fold tuples
Wed, 29 Jul 2009 16:48:34 +0200 haftmann cleaned up abstract tuple operations and named them consistently
Tue, 21 Jul 2009 01:03:18 +0200 wenzelm proper context for Display.pretty_thm etc. or old-style versions Display.pretty_thm_global, Display.pretty_thm_without_context etc.;
Tue, 14 Jul 2009 10:54:04 +0200 haftmann code attributes use common underscore convention
less more (0) -100 -60 tip