Re: [isabelle] value no longer pretty-prints numbers of type nat
Whether this is a bug or a feature, I would not dare to say. I can confirm that in
Isabelle2013, you get pretty numerals for nat, but in Isabelle2013-RC-1, you don't get
them by default. One could argue that the Suc representation is more faithful to the
representation of nat, but for other types like int and rat, they are printed as pretty
If you import HOL/Library/Code_Target_Nat, then you get pretty numerals for nat, too. But
of course, they are then implemented as target-language integers (rather than a datatype
with constructors 0 and Suc).
On 03/10/13 23:34, Christoph LANGE wrote:
with Isabelle 2013-1-RC1,
instead of "1", which, I think, it did yield in Isabelle 2013.
Is this a bug, or is there a new configuration option I need to enable?
This archive was generated by a fusion of
Pipermail (Mailman edition) and