| Tue, 25 Sep 2007 15:34:35 +0200 |
wenzelm |
simplified interpretation setup;
|
file |
diff |
annotate
|
| Tue, 25 Sep 2007 12:16:08 +0200 |
haftmann |
datatype interpretators for size and datatype_realizer
|
file |
diff |
annotate
|
| Tue, 18 Sep 2007 07:46:00 +0200 |
haftmann |
introduced generic concepts for theory interpretators
|
file |
diff |
annotate
|
| Tue, 18 Sep 2007 07:36:15 +0200 |
haftmann |
distinction between regular and default code theorems
|
file |
diff |
annotate
|
| Sat, 15 Sep 2007 19:27:44 +0200 |
haftmann |
clarified class interfaces and internals
|
file |
diff |
annotate
|
| Sat, 25 Aug 2007 09:22:22 +0200 |
haftmann |
made SML/NJ happy
|
file |
diff |
annotate
|
| Fri, 24 Aug 2007 14:14:20 +0200 |
haftmann |
overloaded definitions accompanied by explicit constants
|
file |
diff |
annotate
|
| Fri, 10 Aug 2007 17:04:34 +0200 |
haftmann |
new structure for code generator modules
|
file |
diff |
annotate
|
| Fri, 03 Aug 2007 16:28:15 +0200 |
wenzelm |
replaced Theory.self_ref by Theory.check_thy, which now produces a checked ref;
|
file |
diff |
annotate
|
| Mon, 16 Jul 2007 09:29:04 +0200 |
haftmann |
added function for case certificates
|
file |
diff |
annotate
|
| Tue, 10 Jul 2007 17:30:53 +0200 |
haftmann |
tuned
|
file |
diff |
annotate
|
| Thu, 28 Jun 2007 19:09:35 +0200 |
haftmann |
tuned
|
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
|
| 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
|