| Wed, 04 Mar 2009 10:47:20 +0100 |
nipkow |
Made Option a separate theory and renamed option_map to Option.map
|
file |
diff |
annotate
|
| Wed, 21 Jan 2009 23:40:23 +0100 |
haftmann |
changed import hierarchy
|
file |
diff |
annotate
|
| Wed, 21 Jan 2009 16:47:31 +0100 |
haftmann |
dropped ID
|
file |
diff |
annotate
|
| Sat, 27 Dec 2008 17:49:15 +0100 |
krauss |
removed duplicate sum_case used only by function package;
|
file |
diff |
annotate
|
| Tue, 09 Dec 2008 15:31:38 -0800 |
huffman |
move lemmas from Numeral_Type.thy to other theories
|
file |
diff |
annotate
|
| Fri, 24 Oct 2008 17:51:35 +0200 |
haftmann |
more clever module names for code generation
|
file |
diff |
annotate
|
| Fri, 10 Oct 2008 06:45:53 +0200 |
haftmann |
`code func` now just `code`
|
file |
diff |
annotate
|
| Tue, 07 Oct 2008 16:07:50 +0200 |
haftmann |
arbitrary is undefined
|
file |
diff |
annotate
|
| Thu, 25 Sep 2008 09:28:03 +0200 |
haftmann |
discontinued special treatment of op = vs. eq_class.eq
|
file |
diff |
annotate
|
| Sun, 24 Aug 2008 14:42:22 +0200 |
haftmann |
tuned import order
|
file |
diff |
annotate
|
| Mon, 11 Aug 2008 14:49:53 +0200 |
haftmann |
moved class wellorder to theory Orderings
|
file |
diff |
annotate
|
| Tue, 10 Jun 2008 15:30:33 +0200 |
haftmann |
rep_datatype command now takes list of constructors as input arguments
|
file |
diff |
annotate
|
| Fri, 25 Apr 2008 15:30:33 +0200 |
krauss |
Merged theories about wellfoundedness into one: Wellfounded.thy
|
file |
diff |
annotate
|
| Thu, 20 Mar 2008 12:02:52 +0100 |
haftmann |
Product_Type.apfst and Product_Type.apsnd
|
file |
diff |
annotate
|
| Wed, 19 Mar 2008 22:47:35 +0100 |
wenzelm |
eliminated change_claset/simpset;
|
file |
diff |
annotate
|
| Tue, 26 Feb 2008 20:38:10 +0100 |
haftmann |
tuned proofs
|
file |
diff |
annotate
|
| Fri, 15 Feb 2008 16:09:12 +0100 |
haftmann |
<= and < on nat no longer depend on wellfounded relations
|
file |
diff |
annotate
|
| Sat, 05 Jan 2008 09:16:27 +0100 |
haftmann |
more instantiation
|
file |
diff |
annotate
|
| Mon, 17 Dec 2007 18:22:48 +0100 |
berghofe |
Removed obsolete lemma size_sum.
|
file |
diff |
annotate
|
| Wed, 05 Dec 2007 14:15:45 +0100 |
haftmann |
simplified infrastructure for code generator operational equality
|
file |
diff |
annotate
|
| Fri, 30 Nov 2007 20:13:05 +0100 |
haftmann |
more canonical attribute application
|
file |
diff |
annotate
|
| Thu, 04 Oct 2007 19:54:46 +0200 |
haftmann |
tuned datatype_codegen setup
|
file |
diff |
annotate
|
| Wed, 26 Sep 2007 20:27:55 +0200 |
haftmann |
moved Finite_Set before Datatype
|
file |
diff |
annotate
|
| Tue, 25 Sep 2007 12:16:08 +0200 |
haftmann |
datatype interpretators for size and datatype_realizer
|
file |
diff |
annotate
|
| Wed, 15 Aug 2007 12:52:56 +0200 |
paulson |
ATP blacklisting is now in theory data, attribute noatp
|
file |
diff |
annotate
|
| Thu, 09 Aug 2007 15:52:42 +0200 |
haftmann |
re-eliminated Option.thy
|
file |
diff |
annotate
|
| Tue, 07 Aug 2007 09:38:44 +0200 |
haftmann |
split off theory Option for benefit of code generator
|
file |
diff |
annotate
|
| Wed, 09 May 2007 07:53:06 +0200 |
haftmann |
moved recfun_codegen.ML to Code_Generator.thy
|
file |
diff |
annotate
|
| Tue, 24 Apr 2007 15:18:09 +0200 |
berghofe |
Added intro / elim rules for prod_case.
|
file |
diff |
annotate
|
| Fri, 20 Apr 2007 11:21:42 +0200 |
haftmann |
Isar definitions are now added explicitly to code theorem table
|
file |
diff |
annotate
|
| Wed, 11 Apr 2007 08:28:13 +0200 |
haftmann |
dropped legacy ML bindings
|
file |
diff |
annotate
|
| Fri, 09 Mar 2007 08:45:55 +0100 |
haftmann |
*** empty log message ***
|
file |
diff |
annotate
|
| Fri, 02 Feb 2007 15:47:58 +0100 |
nipkow |
a few additions and deletions
|
file |
diff |
annotate
|
| Wed, 27 Dec 2006 19:09:54 +0100 |
haftmann |
removed code generation stuff belonging to other theories
|
file |
diff |
annotate
|
| Wed, 06 Dec 2006 01:12:36 +0100 |
wenzelm |
removed legacy ML bindings;
|
file |
diff |
annotate
|
| Wed, 22 Nov 2006 10:20:12 +0100 |
haftmann |
dropped eq const
|
file |
diff |
annotate
|
| Sat, 18 Nov 2006 00:20:13 +0100 |
haftmann |
reduced verbosity
|
file |
diff |
annotate
|
| Fri, 17 Nov 2006 02:20:03 +0100 |
wenzelm |
more robust syntax for definition/abbreviation/notation;
|
file |
diff |
annotate
|
| Wed, 08 Nov 2006 13:48:29 +0100 |
wenzelm |
removed theory NatArith (now part of Nat);
|
file |
diff |
annotate
|
| Tue, 31 Oct 2006 14:58:14 +0100 |
haftmann |
adapted seralizer syntax
|
file |
diff |
annotate
|
| Tue, 31 Oct 2006 09:28:54 +0100 |
haftmann |
cleaned up
|
file |
diff |
annotate
|
| Fri, 20 Oct 2006 17:07:27 +0200 |
haftmann |
added reserved words for Haskell
|
file |
diff |
annotate
|
| Fri, 20 Oct 2006 10:44:37 +0200 |
haftmann |
added normal post setup
|
file |
diff |
annotate
|
| Mon, 16 Oct 2006 14:07:31 +0200 |
haftmann |
moved HOL code generator setup to Code_Generator
|
file |
diff |
annotate
|
| Mon, 02 Oct 2006 23:01:14 +0200 |
haftmann |
clarified setup name
|
file |
diff |
annotate
|
| Sun, 01 Oct 2006 22:19:21 +0200 |
wenzelm |
merged with theory Datatype_Universe;
|
file |
diff |
annotate
|
| Sat, 30 Sep 2006 21:39:20 +0200 |
wenzelm |
removed obsolete sum_case_Inl/Inr;
|
file |
diff |
annotate
|
| Tue, 19 Sep 2006 15:21:42 +0200 |
haftmann |
added operational equality
|
file |
diff |
annotate
|
| Wed, 13 Sep 2006 12:05:50 +0200 |
krauss |
Major update to function package, including new syntax and the (only theoretical)
|
file |
diff |
annotate
|
| Fri, 01 Sep 2006 08:36:51 +0200 |
haftmann |
final syntax for some Isar code generator keywords
|
file |
diff |
annotate
|
| Wed, 12 Jul 2006 17:00:22 +0200 |
haftmann |
adaptions in codegen
|
file |
diff |
annotate
|
| Wed, 14 Jun 2006 12:14:42 +0200 |
haftmann |
slight adaption for code generator
|
file |
diff |
annotate
|
| Wed, 07 Jun 2006 16:55:14 +0200 |
haftmann |
slight code generator cleanup
|
file |
diff |
annotate
|
| Tue, 06 Jun 2006 14:56:42 +0200 |
haftmann |
improved code lemmas
|
file |
diff |
annotate
|
| Mon, 05 Jun 2006 14:26:07 +0200 |
krauss |
HOL/Tools/function_package: Added support for mutual recursive definitions.
|
file |
diff |
annotate
|
| Fri, 05 May 2006 17:17:21 +0200 |
krauss |
First usable version of the new function definition package (HOL/function_packake/...).
|
file |
diff |
annotate
|
| Thu, 06 Apr 2006 16:11:30 +0200 |
haftmann |
adapted for definitional code generation
|
file |
diff |
annotate
|
| Tue, 07 Mar 2006 14:09:48 +0100 |
haftmann |
substantial improvement in codegen iml
|
file |
diff |
annotate
|
| Fri, 03 Mar 2006 19:30:20 +0100 |
nipkow |
changed and retracted change of location of code lemmas.
|
file |
diff |
annotate
|
| Mon, 27 Feb 2006 15:51:37 +0100 |
haftmann |
class package and codegen refinements
|
file |
diff |
annotate
|