src/HOL/Tools/inductive_codegen.ML
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
Mon, 29 Jun 2009 12:18:57 +0200 haftmann explicit Set constructor for code generated for sets
Tue, 23 Jun 2009 16:27:12 +0200 haftmann tuned interfaces of datatype module
Fri, 19 Jun 2009 17:23:21 +0200 haftmann discontinued ancient tradition to suffix certain ML module names with "_package"
Sun, 01 Mar 2009 23:36:12 +0100 wenzelm use long names for old-style fold combinators;
Thu, 01 Jan 2009 14:23:39 +0100 wenzelm eliminated OldTerm.(add_)term_consts;
Wed, 31 Dec 2008 18:53:16 +0100 wenzelm moved old add_type_XXX, add_term_XXX etc. to structure OldTerm;
Wed, 31 Dec 2008 00:08:13 +0100 wenzelm moved old add_term_vars, add_term_frees etc. to structure OldTerm;
Thu, 09 Oct 2008 08:47:27 +0200 haftmann established canonical argument order in SML code generators
Sat, 09 Aug 2008 22:43:46 +0200 wenzelm unified Args.T with OuterLex.token, renamed some operations;
Mon, 30 Jun 2008 13:41:33 +0200 haftmann simplified retrieval of theory names of consts and types
Fri, 23 May 2008 16:41:39 +0200 berghofe Replaced Pretty.str and Pretty.string_of by specific functions (from Codegen) that
Sun, 18 May 2008 15:04:09 +0200 wenzelm moved global pretty/string_of functions from Sign to Syntax;
Sat, 17 May 2008 15:31:42 +0200 wenzelm cat_lines;
Sat, 17 May 2008 13:54:30 +0200 wenzelm structure Display: less pervasive operations;
Wed, 07 May 2008 10:57:19 +0200 berghofe Adapted to encoding of sets as predicates
Tue, 18 Sep 2007 07:36:38 +0200 haftmann separated code for inductive sequences from inductive_codegen.ML
Sat, 15 Sep 2007 19:27:35 +0200 haftmann fixed title
Tue, 28 Aug 2007 18:16:06 +0200 berghofe Added sequences with recursion depth limit.
Fri, 10 Aug 2007 17:04:34 +0200 haftmann new structure for code generator modules
Thu, 02 Aug 2007 17:29:40 +0200 berghofe - Added cycle test to function mk_ind_def to avoid non-termination
Wed, 11 Jul 2007 11:38:25 +0200 berghofe Improved code generator for Collect.
Thu, 10 May 2007 10:22:17 +0200 haftmann consts in consts_code Isar commands are now referred to by usual term syntax
Mon, 07 May 2007 00:49:59 +0200 wenzelm simplified DataFun interfaces;
Wed, 25 Apr 2007 15:26:01 +0200 berghofe Moved function params_of to inductive_package.ML.
Fri, 13 Apr 2007 15:43:25 +0200 berghofe Removed erroneous application of rev in get_clauses that caused
Thu, 12 Apr 2007 12:26:19 +0200 haftmann canonical merge operations
Sat, 31 Mar 2007 12:40:55 +0200 berghofe Fixed bug in dest_prem: premises of the form "p x_1 ... x_n"
Mon, 26 Feb 2007 23:18:24 +0100 wenzelm moved eq_thm etc. to structure Thm in Pure/more_thm.ML;
less more (0) -100 -60 tip