[isabelle] Isabelle2014-RC0: Computations with rational numbers



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
Description: Binary data



This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.