Mercurial Mercurial > repos > isabelle / file revisions
summary | shortlog | changelog | graph | tags | bookmarks | branches | file | revisions | annotate | diff | comparison | rss | help
(0) tip
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
src/HOL/Tools/inductive_codegen.ML
Tue, 18 Sep 2007 07:36:38 +0200 haftmann separated code for inductive sequences from inductive_codegen.ML file | diff | annotate
Sat, 15 Sep 2007 19:27:35 +0200 haftmann fixed title file | diff | annotate
Tue, 28 Aug 2007 18:16:06 +0200 berghofe Added sequences with recursion depth limit. file | diff | annotate
Fri, 10 Aug 2007 17:04:34 +0200 haftmann new structure for code generator modules file | diff | annotate
Thu, 02 Aug 2007 17:29:40 +0200 berghofe - Added cycle test to function mk_ind_def to avoid non-termination file | diff | annotate
Wed, 11 Jul 2007 11:38:25 +0200 berghofe Improved code generator for Collect. file | diff | annotate
Thu, 10 May 2007 10:22:17 +0200 haftmann consts in consts_code Isar commands are now referred to by usual term syntax file | diff | annotate
Mon, 07 May 2007 00:49:59 +0200 wenzelm simplified DataFun interfaces; file | diff | annotate
Wed, 25 Apr 2007 15:26:01 +0200 berghofe Moved function params_of to inductive_package.ML. file | diff | annotate
Fri, 13 Apr 2007 15:43:25 +0200 berghofe Removed erroneous application of rev in get_clauses that caused file | diff | annotate
Thu, 12 Apr 2007 12:26:19 +0200 haftmann canonical merge operations file | diff | annotate
Sat, 31 Mar 2007 12:40:55 +0200 berghofe Fixed bug in dest_prem: premises of the form "p x_1 ... x_n" file | diff | annotate
Mon, 26 Feb 2007 23:18:24 +0100 wenzelm moved eq_thm etc. to structure Thm in Pure/more_thm.ML; file | diff | annotate
Wed, 07 Feb 2007 17:44:07 +0100 berghofe Adapted to new inductive definition package. file | diff | annotate
Fri, 13 Oct 2006 18:23:37 +0200 berghofe Moved old inductive package to old_inductive_package.ML file | diff | annotate
Mon, 09 Oct 2006 02:19:49 +0200 wenzelm attribute: Context.mapping; file | diff | annotate
Tue, 11 Jul 2006 12:16:54 +0200 wenzelm replaced Term.variant(list) by Name.variant(_list); file | diff | annotate
Mon, 12 Jun 2006 21:19:00 +0200 wenzelm tuned Seq/Envir/Unify interfaces; file | diff | annotate
Wed, 15 Feb 2006 21:34:55 +0100 wenzelm removed distinct, renamed gen_distinct to distinct; file | diff | annotate
Sun, 12 Feb 2006 21:34:18 +0100 wenzelm simplified TableFun.join; file | diff | annotate
Tue, 07 Feb 2006 19:56:45 +0100 wenzelm renamed gen_duplicates to duplicates; file | diff | annotate
Mon, 06 Feb 2006 20:58:56 +0100 wenzelm replaced Symtab.merge_multi by local merge_rules; file | diff | annotate
Mon, 06 Feb 2006 11:01:28 +0100 haftmann subsituted gen_duplicates / has_duplicates for duplicates whenever appropriate file | diff | annotate
Sat, 21 Jan 2006 23:02:14 +0100 wenzelm simplified type attribute; file | diff | annotate
Thu, 19 Jan 2006 21:22:08 +0100 wenzelm setup: theory -> theory; file | diff | annotate
Tue, 13 Dec 2005 10:39:32 +0100 berghofe list_of_indset now also generates code for set type. file | diff | annotate
Tue, 20 Sep 2005 16:17:34 +0200 haftmann introduced AList module in favor of assoc etc. file | diff | annotate
Thu, 15 Sep 2005 17:16:56 +0200 wenzelm TableFun/Symtab: curried lookup and update; file | diff | annotate
Mon, 05 Sep 2005 17:38:18 +0200 wenzelm curried_lookup/update; file | diff | annotate
Thu, 25 Aug 2005 16:10:16 +0200 berghofe Implemented incremental code generation. file | diff | annotate
Fri, 15 Jul 2005 15:44:15 +0200 wenzelm tuned fold on terms; file | diff | annotate
Fri, 01 Jul 2005 14:13:40 +0200 berghofe Adapted to modular code generation. file | diff | annotate
Fri, 17 Jun 2005 18:33:05 +0200 wenzelm accomodate change of TheoryDataFun; file | diff | annotate
Thu, 07 Apr 2005 09:24:35 +0200 wenzelm handle Option instead of OPTION; file | diff | annotate
Fri, 04 Mar 2005 15:07:34 +0100 skalberg Removed practically all references to Library.foldr. file | diff | annotate
Thu, 03 Mar 2005 12:43:01 +0100 skalberg Move towards standard functions. file | diff | annotate
Sun, 13 Feb 2005 17:15:14 +0100 skalberg Deleted Library.option type. file | diff | annotate
Tue, 26 Oct 2004 16:26:53 +0200 berghofe Added call to Codegen.preprocess. file | diff | annotate
Thu, 23 Sep 2004 10:20:52 +0200 berghofe - Inserted additional check for equality types in check_mode_clause that file | diff | annotate
Tue, 10 Aug 2004 19:10:39 +0200 berghofe Fixed bug in compile_clause that caused equality constraints file | diff | annotate
Mon, 19 Jul 2004 18:14:22 +0200 berghofe Added simple check that allows code generator to produce code containing file | diff | annotate
Fri, 09 Jul 2004 16:33:20 +0200 berghofe - Added support for conditional equations whose premises involve file | diff | annotate
Mon, 21 Jun 2004 10:25:57 +0200 kleing Merged in license change from Isabelle2004 file | diff | annotate
Tue, 01 Jun 2004 14:59:54 +0200 berghofe Adapted to new name mangling function. file | diff | annotate
Wed, 14 Apr 2004 11:44:57 +0200 berghofe Fixed bug in check_mode_clause. file | diff | annotate
Wed, 29 Oct 2003 19:18:15 +0100 berghofe Inserted additional checks in functions dest_prem and add_prod_factors, to file | diff | annotate
Mon, 22 Sep 2003 16:06:05 +0200 berghofe Changed interface of add_attribute. file | diff | annotate
Fri, 22 Aug 2003 11:51:42 +0200 berghofe Improved handling of modes for equality predicate, to avoid ill-typed file | diff | annotate
Thu, 21 Aug 2003 16:20:45 +0200 berghofe Fixed problem with "code ind" attribute that caused code generator to file | diff | annotate
Tue, 07 May 2002 14:26:32 +0200 wenzelm use eq_thm_prop instead of slightly inadequate eq_thm; file | diff | annotate
Thu, 07 Mar 2002 12:03:43 +0100 berghofe - made modes_of more robust file | diff | annotate
Thu, 20 Dec 2001 17:08:55 +0100 berghofe Eliminated "query" syntax. file | diff | annotate
Thu, 20 Dec 2001 15:23:42 +0100 berghofe Fixed bug in function add. file | diff | annotate
Thu, 20 Dec 2001 14:58:18 +0100 berghofe Implemented higher order modes. file | diff | annotate
Mon, 10 Dec 2001 15:40:55 +0100 berghofe - Changed type of invoke_codegen file | diff | annotate
Fri, 31 Aug 2001 18:46:48 +0200 wenzelm tuned headers; file | diff | annotate
Fri, 31 Aug 2001 16:49:06 +0200 berghofe New code generators for HOL. file | diff | annotate
less more (0) tip
isabelle