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

Makarius makarius at sketis.net
Mon Sep 22 22:20:20 CEST 2014

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 
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 

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.


More information about the isabelle-dev mailing list