*To*: isabelle-users at cl.cam.ac.uk*Subject*: [isabelle] Isabelle2014-RC0: Computations with rational numbers*From*: Jose Divasón <jose.divasonm at unirioja.es>*Date*: Wed, 16 Jul 2014 14:44:05 +0200*Sender*: jose.divason at gmail.com

Dear all, I would like to report a minor issue involving rational numbers. Attached and also at the end of this message you can find an example. If one runs such file using Isabelle2013-2, for each value its output shows something like: "-1 / 2" :: "rat" However, in Isabelle2014-RC0 the outputs are different: "Frct (int_of_integer (- 1), 2)" :: "rat" Is this the expected behaviour? I think that everything comes from the following version (the elimination of neg_numeral): http://isabelle.in.tum.de/repos/isabelle/rev/03ff4d1e6784 I have tried to get the former output looking at the print_codeproc and print_codesetup, but I don't see where the problem is. Thanks, Jose theory Foo imports Rat "~~/src/HOL/Library/Code_Target_Numeral" begin value "int_of_integer (- 1)" value "-1::rat" value "(-1/2)::rat" value "(-2/4)::rat" value "-(1/2)::rat" value "(1/-2)::rat" value "Fract (-1) (2)" value "Fract 1 (-2)" end

**Attachment:
Foo.thy**

**Follow-Ups**:**Re: [isabelle] Isabelle2014-RC0: Computations with rational numbers***From:*Florian Haftmann

- Previous by Date: Re: [isabelle] newbie questions: theory for sums and Isar syntax
- Next by Date: Re: [isabelle] Isabelle2014-RC0 segfault / sledgehammer raises exception DUP
- Previous by Thread: Re: [isabelle] Why does unfold fail to work?
- Next by Thread: Re: [isabelle] Isabelle2014-RC0: Computations with rational numbers
- Cl-isabelle-users July 2014 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