src/HOL/Tools/numeral.ML
Fri, 01 Jan 2021 17:35:04 +0100 wenzelm tuned signature -- prefer Isabelle/ML structure Integer;
Fri, 04 Jan 2019 23:22:53 +0100 wenzelm isabelle update -u control_cartouches;
Tue, 24 Apr 2018 14:17:58 +0000 haftmann proper datatype for 8-bit characters
Sat, 12 Mar 2016 22:04:52 +0100 haftmann model characters directly as range 0..255
Thu, 10 Sep 2015 14:12:22 +0200 wenzelm tuned -- avoid slightly odd @{cpat};
Sun, 05 Jul 2015 15:02:30 +0200 wenzelm simplified Thm.instantiate and derivatives: the LHS refers to non-certified variables -- this merely serves as index into already certified structures (or is ignored);
Fri, 06 Mar 2015 23:56:43 +0100 wenzelm clarified context;
Fri, 06 Mar 2015 15:58:56 +0100 wenzelm Thm.cterm_of and Thm.ctyp_of operate on local context;
Wed, 04 Mar 2015 22:05:01 +0100 wenzelm clarified signature;
Sun, 21 Sep 2014 16:56:11 +0200 haftmann explicit separation of signed and unsigned numerals using existing lexical categories num and xnum
Thu, 18 Sep 2014 18:48:04 +0200 haftmann tuned
Sat, 01 Feb 2014 18:42:46 +0100 wenzelm proper context for printing;
Sat, 25 Jan 2014 23:50:49 +0100 haftmann avoid (now superfluous) indirect passing of constant names
Sat, 25 Jan 2014 23:50:49 +0100 haftmann prefer explicit code symbol type over ad-hoc name mangling
Tue, 19 Nov 2013 10:05:53 +0100 haftmann eliminiated neg_numeral in favour of - (numeral _)
Sun, 23 Jun 2013 21:16:07 +0200 haftmann migration from code_(const|type|class|instance) to code_printing and from code_module to code_identifier
Thu, 28 Feb 2013 16:54:52 +0100 wenzelm just one HOLogic.Trueprop_conv, with regular exception CTERM;
Tue, 05 Jun 2012 07:05:56 +0200 haftmann prefer records with speaking labels over deeply nested tuples
Sun, 25 Mar 2012 20:15:39 +0200 huffman merged fork with new numeral representation (see NEWS)
Wed, 15 Feb 2012 23:19:30 +0100 wenzelm renamed Thm.capply to Thm.apply, and Thm.cabs to Thm.lambda in conformance with similar operations in structure Term and Logic;
Tue, 31 Aug 2010 13:29:38 +0200 haftmann more coherent naming of syntax data structures
Mon, 19 Jul 2010 11:55:44 +0200 haftmann distinguish different classes of const syntax
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