src/HOL/Library/Efficient_Nat.thy
Wed, 10 Mar 2010 15:29:22 +0100 haftmann fixed typo
Sun, 07 Mar 2010 12:19:47 +0100 wenzelm modernized structure Object_Logic;
Fri, 22 Jan 2010 13:38:28 +0100 haftmann code literals: distinguish numeral classes by different entries
Thu, 14 Jan 2010 17:54:54 +0100 haftmann dedicated conversions to and from Int
Thu, 14 Jan 2010 17:47:39 +0100 haftmann added Scala setup
Wed, 13 Jan 2010 10:18:45 +0100 haftmann function transformer preprocessor applies to both code generators
Fri, 30 Oct 2009 18:32:40 +0100 haftmann tuned code setup
Thu, 29 Oct 2009 22:16:40 +0100 haftmann adjusted to changes in theory Divides
Wed, 23 Sep 2009 14:00:12 +0200 haftmann Code_Eval(uation)
Fri, 31 Jul 2009 10:49:08 +0200 haftmann repair mess produced by resolution afterwards
Wed, 15 Jul 2009 10:11:13 +0200 haftmann additional preprocessor rule
Tue, 14 Jul 2009 16:27:32 +0200 haftmann prefer code_inline over code_unfold; use code_unfold_post where appropriate
Tue, 14 Jul 2009 10:54:04 +0200 haftmann code attributes use common underscore convention
Tue, 07 Jul 2009 17:37:00 +0200 haftmann Stefan Berghofer's code generator uses Pure equality instead of HOL equality now
Tue, 02 Jun 2009 15:53:05 +0200 haftmann OCaml builtin intergers are elusive; avoid
Sat, 30 May 2009 08:16:44 +0200 haftmann corrected bound/unbounded flag for nat numerals
Tue, 19 May 2009 16:54:55 +0200 haftmann String.literal replaces message_string, code_numeral replaces (code_)index
Tue, 19 May 2009 13:57:32 +0200 haftmann moved Code_Index, Random and Quickcheck before Main
Tue, 12 May 2009 21:17:38 +0200 haftmann adapted to changes in module Code
Mon, 11 May 2009 10:53:19 +0200 haftmann clarified matter of "proper" flag in code equations
Mon, 23 Mar 2009 08:14:24 +0100 haftmann Main is (Complex_Main) base entry point in library theories
Mon, 16 Feb 2009 19:11:16 +0100 haftmann faster preprocessor
Mon, 16 Feb 2009 13:38:09 +0100 haftmann dropped clause_suc_preproc for generic code generator
Fri, 06 Feb 2009 09:05:19 +0100 haftmann mandatory prefix for index conversion operations
Tue, 03 Feb 2009 19:37:00 +0100 haftmann changed name space policy for Haskell includes
Wed, 28 Jan 2009 13:36:11 +0100 haftmann slightly adapted towards more uniformity with div/mod on nat
Thu, 01 Jan 2009 14:23:39 +0100 wenzelm eliminated OldTerm.(add_)term_consts;
Wed, 31 Dec 2008 18:53:16 +0100 wenzelm moved old add_type_XXX, add_term_XXX etc. to structure OldTerm;
Tue, 30 Dec 2008 21:46:48 +0100 wenzelm canonical Term.add_var_names;
Thu, 04 Dec 2008 08:47:45 -0800 huffman change more lemmas to avoid using iszero
Mon, 27 Oct 2008 16:15:49 +0100 haftmann slightly tuned
Fri, 24 Oct 2008 17:48:35 +0200 haftmann more clever module name aliasses for code generation
Fri, 10 Oct 2008 06:45:53 +0200 haftmann `code func` now just `code`
Tue, 07 Oct 2008 16:07:33 +0200 haftmann only one theorem table for both code generators
Tue, 30 Sep 2008 12:49:18 +0200 haftmann clarified codegen interfaces
Thu, 25 Sep 2008 10:17:22 +0200 haftmann non left-linear equations for nbe
Thu, 25 Sep 2008 09:28:03 +0200 haftmann discontinued special treatment of op = vs. eq_class.eq
Tue, 16 Sep 2008 09:21:24 +0200 haftmann evaluation using code generator
Mon, 21 Jul 2008 15:26:24 +0200 haftmann fixed code generator setup
Tue, 15 Jul 2008 16:02:07 +0200 haftmann tuned code theorem bookkeeping
Mon, 14 Jul 2008 11:04:46 +0200 haftmann simpsets as pre/postprocessors; generic preprocessor now named function transformators
Tue, 08 Jul 2008 18:13:09 +0200 haftmann fix: using IntInf.int for SML
Thu, 26 Jun 2008 10:07:01 +0200 haftmann established Plain theory and image
Fri, 28 Mar 2008 22:01:02 +0100 haftmann not depends on Main any longer
Wed, 20 Feb 2008 14:52:34 +0100 haftmann using only an relation predicate to construct div and mod
Tue, 29 Jan 2008 10:19:56 +0100 haftmann treating division by zero properly
Fri, 25 Jan 2008 14:54:46 +0100 haftmann fixed and tuned
Mon, 21 Jan 2008 08:43:31 +0100 haftmann streamlined and improved
Tue, 15 Jan 2008 16:19:23 +0100 haftmann joined theories IntDef, Numeral, IntArith to theory Int
Thu, 10 Jan 2008 19:09:21 +0100 berghofe New interface for test data generators.
Wed, 02 Jan 2008 15:14:23 +0100 haftmann index now a copy of nat rather than int
Thu, 13 Dec 2007 07:09:03 +0100 haftmann target language div and mod
Wed, 28 Nov 2007 15:09:19 +0100 haftmann deleted looping code theorem
Fri, 12 Oct 2007 08:21:09 +0200 haftmann consolidated naming conventions for code generator theories
Tue, 25 Sep 2007 21:08:34 +0200 haftmann Efficient_Nat and Pretty_Int integrated with ML_Int
Tue, 18 Sep 2007 16:08:00 +0200 wenzelm simplified type int (eliminated IntInf.int, integer);
Fri, 24 Aug 2007 14:14:20 +0200 haftmann overloaded definitions accompanied by explicit constants
Fri, 10 Aug 2007 17:10:03 +0200 haftmann new structure for code generator modules
Thu, 09 Aug 2007 15:52:45 +0200 haftmann tuned
Thu, 19 Jul 2007 21:47:39 +0200 haftmann uniform naming conventions for CG theories
less more (0) tip