*To*: cl-isabelle-users at lists.cam.ac.uk*Subject*: Re: [isabelle] Rounding negative fractions in Isabelle*From*: Lars Noschinski <noschinl at in.tum.de>*Date*: Thu, 01 Oct 2015 17:37:00 +0200*In-reply-to*: <560D4F06.8070109@informatik.tu-muenchen.de>*References*: <SNT407-EAS100FCEFEF7FA7A34E451C0DE44C0@phx.gbl> <8040C4EE-FA7D-4550-A0B2-6B0369FC34DA@cam.ac.uk> <560D4F06.8070109@informatik.tu-muenchen.de>*User-agent*: Mozilla/5.0 (X11; Linux x86_64; rv:31.0) Gecko/20100101 Icedove/31.8.0

On 01.10.2015 17:19, Florian Haftmann wrote: > that is easily made plausible: the units of a ring (in case of int, +1 > and -1) form a field. In this segment you expect the conventional rules > of field division to hold: [...] > -1 div -1 = -1 I guess you meant "-1 div -1 = +1"?

**References**:**[isabelle] Rounding negative fractions in Isabelle***From:*Zhe Hou

**Re: [isabelle] Rounding negative fractions in Isabelle***From:*Larry Paulson

**Re: [isabelle] Rounding negative fractions in Isabelle***From:*Florian Haftmann

- Previous by Date: Re: [isabelle] Rounding negative fractions in Isabelle
- Next by Date: Re: [isabelle] Rounding negative fractions in Isabelle
- Previous by Thread: Re: [isabelle] Rounding negative fractions in Isabelle
- Next by Thread: Re: [isabelle] Rounding negative fractions in Isabelle
- Cl-isabelle-users October 2015 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