src/HOL/Tools/numeral_syntax.ML
Fri, 08 Apr 2011 16:34:14 +0200 wenzelm discontinued special treatment of structure Lexicon;
Wed, 06 Apr 2011 14:08:40 +0200 wenzelm discontinued old-style Syntax.constrainC;
Wed, 06 Apr 2011 13:33:46 +0200 wenzelm typed_print_translation: discontinued show_sorts argument;
Wed, 06 Apr 2011 12:58:13 +0200 wenzelm moved unparse material to syntax_phases.ML;
Sun, 05 Sep 2010 21:41:24 +0200 wenzelm turned show_sorts/show_types into proper configuration options;
Wed, 03 Mar 2010 00:32:14 +0100 wenzelm adapted to authentic syntax -- actual types are verbatim;
Thu, 25 Feb 2010 22:17:33 +0100 wenzelm explicit @{type_syntax} markup;
Sat, 13 Feb 2010 23:24:57 +0100 wenzelm modernized structures;
Thu, 11 Feb 2010 23:00:22 +0100 wenzelm modernized translations;
Fri, 02 Jan 2009 19:29:18 +0100 wenzelm removed dead code;
Sun, 17 Feb 2008 06:49:53 +0100 huffman New simpler representation of numerals, using Bit0 and Bit1 instead of BIT, B0, and B1
Tue, 15 Jan 2008 16:19:23 +0100 haftmann joined theories IntDef, Numeral, IntArith to theory Int
Tue, 25 Sep 2007 17:06:14 +0200 wenzelm proper Sign operations instead of Theory aliases;
Tue, 18 Sep 2007 16:08:00 +0200 wenzelm simplified type int (eliminated IntInf.int, integer);
Thu, 17 May 2007 19:49:40 +0200 haftmann canonical prefixing of class constants
Wed, 13 Dec 2006 15:45:33 +0100 haftmann authentic syntax for number_of
Tue, 12 Dec 2006 12:03:46 +0100 wenzelm make SML/NJ happy;
Tue, 12 Dec 2006 00:25:05 +0100 wenzelm authentic syntax for Pls/Min/Bit;
Sun, 10 Dec 2006 22:27:06 +0100 wenzelm tuned comments;
Tue, 11 Jul 2006 14:21:05 +0200 wenzelm removed str_to_int in favour of general Syntax.read_xnum;
Tue, 11 Jul 2006 00:43:54 +0200 kleing hex and binary numerals (contributed by Rafal Kolanski)
Thu, 27 Apr 2006 12:11:56 +0200 paulson renamed HOLogic.mk_bin to mk_binum for consistency with dest_binum
Sun, 09 Apr 2006 18:51:15 +0200 wenzelm hide consts in Numeral.thy;
Thu, 19 Jan 2006 21:22:08 +0100 wenzelm setup: theory -> theory;
Sat, 11 Jun 2005 22:15:50 +0200 wenzelm Theory.hide_consts renamed to Theory.hide_consts_i;
Mon, 16 May 2005 10:29:15 +0200 paulson Use of IntInf.int instead of int in most numeric simprocs; avoids
Wed, 23 Mar 2005 12:09:18 +0100 paulson replaced bool by a new datatype "bit" for binary numerals
Tue, 08 Mar 2005 16:02:52 +0100 obua fix integer overflow in numeral syntax for SML NJ.
Thu, 01 Jul 2004 12:29:53 +0200 paulson new treatment of binary numerals
Mon, 21 Jun 2004 10:25:57 +0200 kleing Merged in license change from Isabelle2004
Tue, 13 Aug 2002 12:16:14 +0200 wenzelm more robust printing of numerals;
Mon, 12 Aug 2002 17:48:19 +0200 nipkow *** empty log message ***
Tue, 07 May 2002 14:28:34 +0200 wenzelm be liberal about missing types;
Fri, 05 Oct 2001 21:52:39 +0200 wenzelm sane numerals (stage 1): added generic 1, removed 1' and 2 on nat,
Wed, 08 Aug 2001 17:38:29 +0200 wenzelm constify numeral tokens in order to allow translations;
Fri, 12 Jan 2001 20:03:26 +0100 wenzelm hide dest_bin;
Mon, 18 Dec 2000 14:59:05 +0100 nipkow moved mk_bin from Numerals to HOLogic
Thu, 13 Jul 2000 23:11:38 +0200 wenzelm use Syntax.read_xnum;
Sat, 01 Jul 2000 19:55:22 +0200 wenzelm GPLed;
Tue, 21 Sep 1999 14:14:14 +0200 nipkow moved inf_of(?) to hologic.
Wed, 01 Sep 1999 21:26:26 +0200 wenzelm observe show_types;
Fri, 23 Jul 1999 17:30:27 +0200 paulson now using correctly-typed constants from HOLogic
Wed, 21 Jul 1999 15:18:36 +0200 paulson now exports mk_bin
Tue, 06 Jul 1999 21:08:30 +0200 wenzelm added Numeral.thy, Tools/numeral_syntax.ML;
less more (0) tip