Support for negative literals in Isabelle

drivers/isabelle-common.gen

@@ -6,6 +6,7 @@ valid "Finished Why3 theory"
 fail "\\*\\*\\* \\(.*\\)$" "\\1"
 time "why3cpulimit time : %s s"
 
+transformation "eliminate_negative_constants"
 transformation "eliminate_epsilon"
 transformation "eliminate_if_fmla"
 transformation "eliminate_let_fmla"

src/printer/isabelle.ml

@@ -200,13 +200,13 @@ let rec print_term info defs fmt t = match t.t_node with
       let number_format = {
           Number.long_int_support = true;
           Number.extra_leading_zeros_support = true;
-          Number.negative_int_support = Number.Number_default;
+          Number.negative_int_support = Number.Number_unsupported;
           Number.dec_int_support = Number.Number_default;
           Number.hex_int_support = Number.Number_unsupported;
           Number.oct_int_support = Number.Number_unsupported;
           Number.bin_int_support = Number.Number_unsupported;
           Number.def_int_support = Number.Number_unsupported;
-          Number.negative_real_support = Number.Number_default;
+          Number.negative_real_support = Number.Number_unsupported;
           Number.dec_real_support = Number.Number_unsupported;
           Number.hex_real_support = Number.Number_unsupported;
           Number.frac_real_support = Number.Number_custom