*To*: Andreas Lochbihler <lochbihl at ipd.info.uni-karlsruhe.de>*Subject*: Re: [isabelle] Hidding the "int", "nat" and "real" conversion functions*From*: Johannes Hoelzl <hoelzl at in.tum.de>*Date*: Thu, 22 Jan 2009 12:14:42 +0100*Cc*: isabelle-users at cl.cam.ac.uk*In-reply-to*: <497847D8.8040905@ipd.info.uni-karlsruhe.de>*Organization*: TU München*References*: <1232558290.27529.20.camel@macbroy24.informatik.tu-muenchen.de> <497847D8.8040905@ipd.info.uni-karlsruhe.de>

Hi Andreas, > But this is probably not, what you wanted because the parenthesis ? around > a+b are missing, so set the precedence of the parameter to 66 (+ has 65 > and * 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

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

**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

- Previous by Date: [isabelle] parameters of function definitions and scope of constants
- Next by Date: Re: [isabelle] Hidding the "int", "nat" and "real" conversion functions
- 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