src/HOL/Decision_Procs/MIR.thy

       by (simp only: real_of_int_mult real_of_int_add real_of_int_inject[symmetric] ei[simplified isint_iff] real_of_one) 
         (simp add: algebra_simps)
     hence "\<exists> j1\<in> {1 .. c*d}. real (c*i) = (- ?N i e + real j1) - 1"
       by (simp only: algebra_simps)
         hence "\<exists> j1\<in> {1 .. c*d}. real (c*i) = - 1 - ?N i e + real j1"
-          by (simp add: algebra_simps minus_one [symmetric] del: minus_one)
+          by (simp add: algebra_simps)
     with nob  have ?case by blast }
   ultimately show ?case by blast
 next
   case (9 j c e)  hence p: "real j rdvd real (c*i) + ?N i e" (is "?p x") and cp: "c > 0" and bn:"numbound0 e"  by simp+
   let ?e = "Inum (real i # bs) e"

       | SOME n => mk_Bound n)
   | num_of_term vs @{term "real (0::int)"} = mk_C 0
   | num_of_term vs @{term "real (1::int)"} = mk_C 1
   | num_of_term vs @{term "0::real"} = mk_C 0
   | num_of_term vs @{term "1::real"} = mk_C 1
+  | num_of_term vs @{term "- 1::real"} = mk_C (~ 1)
   | num_of_term vs (Bound i) = mk_Bound i
   | num_of_term vs (@{term "uminus :: real \<Rightarrow> real"} $ t') = @{code Neg} (num_of_term vs t')
   | num_of_term vs (@{term "op + :: real \<Rightarrow> real \<Rightarrow> real"} $ t1 $ t2) =
       @{code Add} (num_of_term vs t1, num_of_term vs t2)
   | num_of_term vs (@{term "op - :: real \<Rightarrow> real \<Rightarrow> real"} $ t1 $ t2) =

       (case (num_of_term vs t1)
        of @{code C} i => @{code Mul} (i, num_of_term vs t2)
         | _ => error "num_of_term: unsupported Multiplication")
   | num_of_term vs (@{term "real :: int \<Rightarrow> real"} $ (@{term "numeral :: _ \<Rightarrow> int"} $ t')) =
       mk_C (HOLogic.dest_num t')
-  | num_of_term vs (@{term "real :: int \<Rightarrow> real"} $ (@{term "neg_numeral :: _ \<Rightarrow> int"} $ t')) =
+  | num_of_term vs (@{term "real :: int \<Rightarrow> real"} $ (@{term "- numeral :: _ \<Rightarrow> int"} $ t')) =
       mk_C (~ (HOLogic.dest_num t'))
   | num_of_term vs (@{term "real :: int \<Rightarrow> real"} $ (@{term "floor :: real \<Rightarrow> int"} $ t')) =
       @{code Floor} (num_of_term vs t')
   | num_of_term vs (@{term "real :: int \<Rightarrow> real"} $ (@{term "ceiling :: real \<Rightarrow> int"} $ t')) =
       @{code Neg} (@{code Floor} (@{code Neg} (num_of_term vs t')))
   | num_of_term vs (@{term "numeral :: _ \<Rightarrow> real"} $ t') =
       mk_C (HOLogic.dest_num t')
-  | num_of_term vs (@{term "neg_numeral :: _ \<Rightarrow> real"} $ t') =
+  | num_of_term vs (@{term "- numeral :: _ \<Rightarrow> real"} $ t') =
       mk_C (~ (HOLogic.dest_num t'))
   | num_of_term vs t = error ("num_of_term: unknown term " ^ Syntax.string_of_term @{context} t);
 
 fun fm_of_term vs @{term True} = @{code T}
   | fm_of_term vs @{term False} = @{code F}

       @{code Le} (@{code Sub} (num_of_term vs t1, num_of_term vs t2))
   | fm_of_term vs (@{term "op = :: real \<Rightarrow> real \<Rightarrow> bool"} $ t1 $ t2) =
       @{code Eq} (@{code Sub} (num_of_term vs t1, num_of_term vs t2)) 
   | fm_of_term vs (@{term "op rdvd"} $ (@{term "real :: int \<Rightarrow> real"} $ (@{term "numeral :: _ \<Rightarrow> int"} $ t1)) $ t2) =
       mk_Dvd (HOLogic.dest_num t1, num_of_term vs t2)
-  | fm_of_term vs (@{term "op rdvd"} $ (@{term "real :: int \<Rightarrow> real"} $ (@{term "neg_numeral :: _ \<Rightarrow> int"} $ t1)) $ t2) =
+  | fm_of_term vs (@{term "op rdvd"} $ (@{term "real :: int \<Rightarrow> real"} $ (@{term "- numeral :: _ \<Rightarrow> int"} $ t1)) $ t2) =
       mk_Dvd (~ (HOLogic.dest_num t1), num_of_term vs t2)
   | fm_of_term vs (@{term "op = :: bool \<Rightarrow> bool \<Rightarrow> bool"} $ t1 $ t2) =
       @{code Iff} (fm_of_term vs t1, fm_of_term vs t2)
   | fm_of_term vs (@{term HOL.conj} $ t1 $ t2) =
       @{code And} (fm_of_term vs t1, fm_of_term vs t2)