Mercurialisabelle / file revisions
summary | shortlog | changelog | graph | tags | branches | file | revisions | annotate | diff | rss
src/HOL/Tools/numeral_syntax.ML
2007-05-17 haftmann 2007-05-17 canonical prefixing of class constants file | diff | annotate
2006-12-13 haftmann 2006-12-13 authentic syntax for number_of file | diff | annotate
2006-12-12 wenzelm 2006-12-12 make SML/NJ happy; file | diff | annotate
2006-12-12 wenzelm 2006-12-12 authentic syntax for Pls/Min/Bit; separated translation functions from HOLogic functionality; file | diff | annotate
2006-12-10 wenzelm 2006-12-10 tuned comments; file | diff | annotate
2006-07-11 wenzelm 2006-07-11 removed str_to_int in favour of general Syntax.read_xnum; file | diff | annotate
2006-07-11 kleing 2006-07-11 hex and binary numerals (contributed by Rafal Kolanski) file | diff | annotate
2006-04-27 paulson 2006-04-27 renamed HOLogic.mk_bin to mk_binum for consistency with dest_binum file | diff | annotate
2006-04-09 wenzelm 2006-04-09 hide consts in Numeral.thy; file | diff | annotate
2006-01-19 wenzelm 2006-01-19 setup: theory -> theory; file | diff | annotate
2005-06-11 wenzelm 2005-06-11 Theory.hide_consts renamed to Theory.hide_consts_i; file | diff | annotate
2005-05-16 paulson 2005-05-16 Use of IntInf.int instead of int in most numeric simprocs; avoids integer overflow in SML/NJ file | diff | annotate
2005-03-23 paulson 2005-03-23 replaced bool by a new datatype "bit" for binary numerals file | diff | annotate
2005-03-08 obua 2005-03-08 fix integer overflow in numeral syntax for SML NJ. file | diff | annotate
2004-07-01 paulson 2004-07-01 new treatment of binary numerals file | diff | annotate
2004-06-21 kleing 2004-06-21 Merged in license change from Isabelle2004 file | diff | annotate
2002-08-13 wenzelm 2002-08-13 more robust printing of numerals; file | diff | annotate
2002-08-12 nipkow 2002-08-12 *** empty log message *** file | diff | annotate
2002-05-07 wenzelm 2002-05-07 be liberal about missing types; file | diff | annotate
2001-10-05 wenzelm 2001-10-05 sane numerals (stage 1): added generic 1, removed 1' and 2 on nat, "num" syntax (still with "#"), Numeral0, Numeral1; file | diff | annotate
2001-08-08 wenzelm 2001-08-08 constify numeral tokens in order to allow translations; file | diff | annotate
2001-01-12 wenzelm 2001-01-12 hide dest_bin; file | diff | annotate
2000-12-18 nipkow 2000-12-18 moved mk_bin from Numerals to HOLogic first steps towards rational lin arith file | diff | annotate
2000-07-13 wenzelm 2000-07-13 use Syntax.read_xnum; file | diff | annotate
2000-07-01 wenzelm 2000-07-01 GPLed; file | diff | annotate
1999-09-21 nipkow 1999-09-21 moved inf_of(?) to hologic. file | diff | annotate
1999-09-01 wenzelm 1999-09-01 observe show_types; file | diff | annotate
1999-07-23 paulson 1999-07-23 now using correctly-typed constants from HOLogic file | diff | annotate
1999-07-21 paulson 1999-07-21 now exports mk_bin file | diff | annotate
1999-07-06 wenzelm 1999-07-06 added Numeral.thy, Tools/numeral_syntax.ML; file | diff | annotate
isabelle