# HG changeset patch
# User nipkow
# Date 1470404693 -7200
# Node ID d0fa16751d149a72ba2bedcd2ea136b1ece07197
# Parent  f560147710fbd5c6eb67ebf92c05bf9565a842bc
fixed floor proof

diff -r f560147710fb -r d0fa16751d14 src/HOL/Decision_Procs/MIR.thy
--- a/src/HOL/Decision_Procs/MIR.thy	Fri Aug 05 12:27:51 2016 +0200
+++ b/src/HOL/Decision_Procs/MIR.thy	Fri Aug 05 15:44:53 2016 +0200
@@ -1526,7 +1526,7 @@
   also have "\<dots> = real_of_int \<lfloor>real_of_int ?nt * real_of_int x + ?I x ?at\<rfloor>" by simp
   also have "\<dots> = real_of_int \<lfloor>?I x ?at + real_of_int (?nt * x)\<rfloor>" by (simp add: ac_simps)
   also have "\<dots> = real_of_int (\<lfloor>?I x ?at\<rfloor> + (?nt * x))"
-    using floor_add_of_int[of "?I x ?at" "?nt * x"] by simp
+    by (simp add: of_int_mult[symmetric] del: of_int_mult)
   also have "\<dots> = real_of_int (?nt)*(real_of_int x) + real_of_int \<lfloor>?I x ?at\<rfloor>" by (simp add: ac_simps)
   finally have "?I x (Floor t) = ?I x (CN 0 n a)" using th by simp
   with na show ?case by simp