Nothing fancy, just a couple of code_post rules to rewrite successor
notation into numeral notation after evaluation and before printing. I
don't know if there's a better way to do that, but I think we discussed
this on the mailing list a while ago and came to the conclusion that
code_post is indeed the way to go.

Of course, I am always open to better solutions, perhaps avoiding the
successor notation entirely, but I don't know the code generator well
enough to say if this is possible (or where the successor stuff comes
from in the first place)

In any case, I would argue that even those code_post rules to rewrite
successor notation to numerals is a lot better than what we have at the


On 2017-07-05 21:45, Lawrence Paulson wrote:
> What’s the idea here?
> Larry
>> On 5 Jul 2017, at 21:09, Manuel Eberl <> wrote:
>> the proper printing of "nat" values as numerals instead of successor 
>> notation.

isabelle-dev mailing list

Reply via email to