[isabelle] value "set [0,0::nat]" = "{0, 0}"::"nat set" – a bug?

Dear Isabelle developers,

in Isabelle2013 the expression

value "set [0,0::nat]"

evaluates to

"{0, 0}"
  :: "nat set"

Looks like a bug to me.  Even more so because

value "{0, 0}::(nat set)"


  :: "nat set"

as expected.

Cheers, and have a nice weekend,


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.

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