[isabelle] value no longer pretty-prints numbers of type nat



Hi all,

with Isabelle 2013-1-RC1,

value "1::nat"

yields

"Suc 0"
  :: "nat"

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?

Cheers,

Christoph

-- 
Christoph Lange, School of Computer Science, University of Birmingham
http://cs.bham.ac.uk/~langec/, Skype duke4701

→ Mathematics in Computer Science Special Issue on “Enabling Domain
  Experts to use Formalised Reasoning”; submission until 31 October.
  http://cs.bham.ac.uk/research/projects/formare/pubs/mcs-doform/




This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.