src/HOL/Tools/numeral.ML
Fri, 22 Jan 2010 13:38:28 +0100 haftmann code literals: distinguish numeral classes by different entries
Thu, 14 Jan 2010 17:47:38 +0100 haftmann allow individual printing of numerals during code serialization
Fri, 04 Dec 2009 18:19:31 +0100 haftmann more speaking function names for Code_Printer; added doublesemicolon
Wed, 15 Jul 2009 23:48:21 +0200 wenzelm more antiquotations;
Tue, 02 Jun 2009 15:53:03 +0200 haftmann tuned whitespace
Wed, 06 May 2009 19:09:31 +0200 haftmann robustifed infrastructure for complex term syntax during code generation
Wed, 29 Oct 2008 11:33:40 +0100 haftmann explicit check for pattern discipline before code translation
Wed, 22 Oct 2008 14:15:45 +0200 haftmann code identifier namings are no longer imperative
Mon, 22 Sep 2008 08:00:24 +0200 haftmann fixed headers
Wed, 17 Sep 2008 21:27:08 +0200 wenzelm back to dynamic the_context(), because static @{theory} is invalidated if ML environment changes within the same code block;
Tue, 02 Sep 2008 20:38:17 +0200 haftmann distributed literal code generation out of central infrastructure
Mon, 01 Sep 2008 10:18:37 +0200 haftmann restructured code generation of literals
Thu, 28 Aug 2008 22:09:20 +0200 haftmann restructured and split code serializer module
Sun, 17 Feb 2008 06:49:53 +0100 huffman New simpler representation of numerals, using Bit0 and Bit1 instead of BIT, B0, and B1
Fri, 25 Jan 2008 14:54:46 +0100 haftmann fixed and tuned
Mon, 21 Jan 2008 08:43:32 +0100 haftmann explicit auxiliary function for code setup
Tue, 15 Jan 2008 16:19:23 +0100 haftmann joined theories IntDef, Numeral, IntArith to theory Int
Tue, 18 Sep 2007 16:08:00 +0200 wenzelm simplified type int (eliminated IntInf.int, integer);
Thu, 05 Jul 2007 00:06:12 +0200 wenzelm Logical operations on numerals (see also HOL/hologic.ML).
less more (0) tip