*To*: Johannes Hoelzl <hoelzl at in.tum.de>*Subject*: Re: [isabelle] Hidding the "int", "nat" and "real" conversion functions*From*: Andreas Lochbihler <lochbihl at ipd.info.uni-karlsruhe.de>*Date*: Thu, 22 Jan 2009 12:41:26 +0100*Cc*: isabelle-users at cl.cam.ac.uk*In-reply-to*: <1232622882.8230.12.camel@macbroy24.informatik.tu-muenchen.de>*References*: <1232558290.27529.20.camel@macbroy24.informatik.tu-muenchen.de> <497847D8.8040905@ipd.info.uni-karlsruhe.de> <1232622882.8230.12.camel@macbroy24.informatik.tu-muenchen.de>*User-agent*: Thunderbird 2.0.0.17 (X11/20080925)

Hi Johannes,

notation (output) int ("_" [1000] 1000) This should work for all of your examples, but: term "x * int (a * b) + f (int a)" produces: "x * (a * b) + f a" Regards, Andreas Johannes Hoelzl schrieb:

Hi Andreas,But this is probably not, what you wanted because the parenthesis ? arounda+b are missing, so set the precedence of the parameter to 66 (+ has 65and * 70):notation (output) int ("_" [66] 1000) term "x * int (a + b) + f (int a)" (* output: "x * (a + b) + f a" *)Wow, great! Works perfectly for me. I discoverd just a small flaw: notation (output) int ("_" [66] 1000) term "f (int (g a))" (* output: "f g a" *) notation (output) int ("_" [66] 999) term "f (int (g a))" (* output: "f g a" *) term "f (int (a + a))" (* output: "f ((a + a))" *) Hence the parenthesis around "g a" is missing. When the precedence is decreased the additional parenthesis is again shown. So it is probably not enough as a replacement for the set-hidding in "HOL/Library/OptionalSugar.thy". Regards, Johannes

**References**:**[isabelle] Hidding the "int", "nat" and "real" conversion functions***From:*Johannes Hoelzl

**Re: [isabelle] Hidding the "int", "nat" and "real" conversion functions***From:*Andreas Lochbihler

**Re: [isabelle] Hidding the "int", "nat" and "real" conversion functions***From:*Johannes Hoelzl

- Previous by Date: Re: [isabelle] Hidding the "int", "nat" and "real" conversion functions
- Next by Date: [isabelle] "The QED Project"
- Previous by Thread: Re: [isabelle] Hidding the "int", "nat" and "real" conversion functions
- Next by Thread: Re: [isabelle] Hidding the "int", "nat" and "real" conversion functions
- Cl-isabelle-users January 2009 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