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
|
Tue, 24 Apr 2007 15:13:19 +0200 |
berghofe |
Streamlined datatype_codegen function using new datatype_of_case
|
file |
diff |
annotate
|
Fri, 20 Apr 2007 11:21:48 +0200 |
haftmann |
cleared dead code
|
file |
diff |
annotate
|
Wed, 04 Apr 2007 00:11:03 +0200 |
wenzelm |
removed obsolete sign_of/sign_of_thm;
|
file |
diff |
annotate
|
Tue, 03 Apr 2007 19:24:10 +0200 |
wenzelm |
ranamed CodegenData.lazy to lazy_thms (avoid clash with Alice keywords);
|
file |
diff |
annotate
|
Fri, 30 Mar 2007 16:19:03 +0200 |
haftmann |
simplified constant representation in code generator
|
file |
diff |
annotate
|
Tue, 20 Mar 2007 15:52:37 +0100 |
haftmann |
switched exception from arbitrary to undefined
|
file |
diff |
annotate
|
Sun, 11 Mar 2007 15:02:44 +0100 |
haftmann |
clarified code
|
file |
diff |
annotate
|
Sat, 10 Mar 2007 16:13:08 +0100 |
berghofe |
Eta-expanded codetype_hook to make SML/NJ happy.
|
file |
diff |
annotate
|
Fri, 09 Mar 2007 08:45:53 +0100 |
haftmann |
dropped code datatype certificates
|
file |
diff |
annotate
|
Fri, 16 Feb 2007 22:13:15 +0100 |
wenzelm |
unified arity parser/arguments;
|
file |
diff |
annotate
|
Sat, 10 Feb 2007 09:26:15 +0100 |
haftmann |
canonical interface for attributes
|
file |
diff |
annotate
|
Thu, 25 Jan 2007 09:32:34 +0100 |
haftmann |
adjusted names
|
file |
diff |
annotate
|
Wed, 10 Jan 2007 09:28:24 +0100 |
haftmann |
improved case patterns
|
file |
diff |
annotate
|
Wed, 10 Jan 2007 08:58:35 +0100 |
haftmann |
added undefined in cases
|
file |
diff |
annotate
|
Tue, 09 Jan 2007 19:08:58 +0100 |
haftmann |
handling for "undefined" in case expressions
|
file |
diff |
annotate
|
Fri, 29 Dec 2006 12:11:00 +0100 |
haftmann |
simplified class_package
|
file |
diff |
annotate
|
Thu, 07 Dec 2006 23:16:55 +0100 |
wenzelm |
reorganized structure Tactic vs. MetaSimplifier;
|
file |
diff |
annotate
|
Tue, 28 Nov 2006 00:35:18 +0100 |
wenzelm |
simplified '?' operator;
|
file |
diff |
annotate
|
Mon, 27 Nov 2006 13:42:33 +0100 |
haftmann |
removed HOL structure
|
file |
diff |
annotate
|
Fri, 24 Nov 2006 22:05:12 +0100 |
wenzelm |
ProofContext.init;
|
file |
diff |
annotate
|
Wed, 22 Nov 2006 10:20:12 +0100 |
haftmann |
dropped eq const
|
file |
diff |
annotate
|
Mon, 16 Oct 2006 14:07:31 +0200 |
haftmann |
moved HOL code generator setup to Code_Generator
|
file |
diff |
annotate
|
Fri, 13 Oct 2006 16:52:47 +0200 |
haftmann |
tuned
|
file |
diff |
annotate
|
Wed, 04 Oct 2006 14:17:46 +0200 |
haftmann |
clarified header comments
|
file |
diff |
annotate
|
Mon, 02 Oct 2006 23:00:51 +0200 |
haftmann |
tuned
|
file |
diff |
annotate
|
Fri, 22 Sep 2006 14:36:23 +0200 |
berghofe |
Fixed bug concerning the generation of identifiers for
|
file |
diff |
annotate
|
Tue, 19 Sep 2006 15:44:04 +0200 |
haftmann |
removed diagnostic messages
|
file |
diff |
annotate
|
Tue, 19 Sep 2006 15:22:05 +0200 |
haftmann |
code generation 2 adjustments
|
file |
diff |
annotate
|
Wed, 30 Aug 2006 15:11:17 +0200 |
haftmann |
code refinements
|
file |
diff |
annotate
|
Wed, 30 Aug 2006 08:30:09 +0200 |
haftmann |
fixes
|
file |
diff |
annotate
|
Tue, 29 Aug 2006 14:31:13 +0200 |
haftmann |
added typecopy_package
|
file |
diff |
annotate
|
Thu, 17 Aug 2006 09:24:47 +0200 |
haftmann |
cleanup
|
file |
diff |
annotate
|
Mon, 14 Aug 2006 13:46:16 +0200 |
haftmann |
added add_hook_bootstrap
|
file |
diff |
annotate
|
Tue, 25 Jul 2006 16:51:26 +0200 |
haftmann |
renamed Name.give_names to Name.names and moved Name.alphanum to Symbol.alphanum
|
file |
diff |
annotate
|
Tue, 25 Jul 2006 16:43:33 +0200 |
haftmann |
fixed typo
|
file |
diff |
annotate
|
Sun, 23 Jul 2006 07:19:26 +0200 |
haftmann |
tactic for prove_instance_arity now gets definition theorems as arguments
|
file |
diff |
annotate
|
Fri, 21 Jul 2006 14:47:22 +0200 |
haftmann |
hooks now take string list as arguments (mutual datatypes); some nice combinators in datatype_codegen
|
file |
diff |
annotate
|
Wed, 12 Jul 2006 17:00:22 +0200 |
haftmann |
adaptions in codegen
|
file |
diff |
annotate
|
Tue, 11 Jul 2006 12:16:54 +0200 |
wenzelm |
replaced Term.variant(list) by Name.variant(_list);
|
file |
diff |
annotate
|
Wed, 14 Jun 2006 12:12:01 +0200 |
haftmann |
added hook for case const defs
|
file |
diff |
annotate
|
Wed, 07 Jun 2006 16:55:39 +0200 |
haftmann |
adding case theorems for code generator
|
file |
diff |
annotate
|
Tue, 09 May 2006 10:09:37 +0200 |
haftmann |
added DatatypeHooks
|
file |
diff |
annotate
|
Mon, 24 Apr 2006 16:37:37 +0200 |
haftmann |
more precise tactics
|
file |
diff |
annotate
|
Thu, 06 Apr 2006 16:10:46 +0200 |
haftmann |
cleanup in datatype package
|
file |
diff |
annotate
|
Fri, 10 Feb 2006 09:09:07 +0100 |
haftmann |
improved code generator devarification
|
file |
diff |
annotate
|
Tue, 07 Feb 2006 08:47:43 +0100 |
haftmann |
slight improvements in code generation
|
file |
diff |
annotate
|
Tue, 31 Jan 2006 16:15:51 +0100 |
haftmann |
minor change to CodegenPackage interface
|
file |
diff |
annotate
|
Thu, 19 Jan 2006 21:22:08 +0100 |
wenzelm |
setup: theory -> theory;
|
file |
diff |
annotate
|
Tue, 17 Jan 2006 16:36:57 +0100 |
haftmann |
substantial improvements in code generator
|
file |
diff |
annotate
|
Thu, 29 Dec 2005 15:31:10 +0100 |
haftmann |
adaptions to changes in code generator
|
file |
diff |
annotate
|
Wed, 21 Dec 2005 15:18:17 +0100 |
haftmann |
slight clean ups
|
file |
diff |
annotate
|
Mon, 12 Dec 2005 15:37:35 +0100 |
haftmann |
improvement in eq handling
|
file |
diff |
annotate
|
Fri, 09 Dec 2005 15:25:29 +0100 |
haftmann |
improved extraction interface
|
file |
diff |
annotate
|
Fri, 02 Dec 2005 16:05:12 +0100 |
haftmann |
adjusted to improved code generator interface
|
file |
diff |
annotate
|
Fri, 25 Nov 2005 17:41:52 +0100 |
haftmann |
code generator: case expressions, improved name resolving
|
file |
diff |
annotate
|
Tue, 22 Nov 2005 12:59:25 +0100 |
haftmann |
added codegenerator
|
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
|