*To*: Steven Obua <obua at in.tum.de>*Subject*: Re: [isabelle] Numeral is acting strangely*From*: Rafal Kolanski <rafalk at cse.unsw.edu.au>*Date*: Tue, 04 Jul 2006 21:03:34 +1000*Cc*: isabelle-users at cl.cam.ac.uk*In-reply-to*: <44AA423E.4060803@in.tum.de>*References*: <44A8DB95.7010908@cse.unsw.edu.au> <44AA36C3.3010907@in.tum.de> <44AA3DCB.5040401@cse.unsw.edu.au> <44AA423E.4060803@in.tum.de>*User-agent*: Thunderbird 1.5.0.4 (Windows/20060516)

Steven Obua wrote:

"2::'a" is just a pretty-printed version of a more complex term. Youcannot pretty-print "Numeral0" in that way, because then "Numeral0"would have to become "0", but as you already figured out, "Numeral0" isnot the same as "0", therefore this pretty-printing would be maybeintuitive, but wrong.

Rafal Kolanski.

**References**:**[isabelle] Numeral is acting strangely***From:*Rafal Kolanski

**Re: [isabelle] Numeral is acting strangely***From:*Steven Obua

**Re: [isabelle] Numeral is acting strangely***From:*Rafal Kolanski

**Re: [isabelle] Numeral is acting strangely***From:*Steven Obua

- Previous by Date: Re: [isabelle] Numeral is acting strangely
- Next by Date: Re: [isabelle] Numeral is acting strangely
- Previous by Thread: Re: [isabelle] Numeral is acting strangely
- Next by Thread: [isabelle] Recdef or Inductive
- Cl-isabelle-users July 2006 archives indexes sorted by: [ thread ] [ subject ] [ author ] [ date ]
- Cl-isabelle-users list archive Table of Contents
- More information about the Cl-isabelle-users mailing list