[isabelle-dev] NEWS: Lexically unsigned numerals for HOL

[Makarius]

On Mon, 22 Sep 2014, Makarius wrote:

> Looking once again at ZF xnum syntax, I think it can be expressed 
> without the xnum token, and without any syntax change for now -- that 
> may be reconsidered independently.

See now:

changeset:   58420:37cbbd8eb460
user:        wenzelm
date:        Mon Sep 22 21:28:57 2014 +0200
files:       NEWS src/Doc/Isar_Ref/Inner_Syntax.thy src/HOL/Num.thy 
src/Pure/Syntax/lexicon.ML src/Pure/pure_thy.ML src/ZF/Bin.thy 
src/ZF/Tools/numeral_syntax.ML
description:
discontinued old "xnum" token category;
simplified Lexicon.read_num, Lexicon.read_float: no sign here;
express ZF numerals via "num" with mixfix grammar;
recovered printing of ZF numerals: "one" is abbreviation;


The last item means that printing of #42 etc. now works again, after many 
years of being broken by accident.  This shows that nobody has used that 
seriously.

Larry can say what # vs. $ is meant to be.  With the mixfix grammar around 
regular "num" it should be easy to change that -- or leave it unchanged.


 	Makarius