| 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
|