# HG changeset patch
# User haftmann
# Date 1429292980 -7200
# Node ID 3d696ccb7fa6f816136e55675d1eef541618ccaf
# Parent  b758c99371604bc956679713d96719b23a010f09
compactified proposition

diff -r b758c9937160 -r 3d696ccb7fa6 src/HOL/Archimedean_Field.thy
--- a/src/HOL/Archimedean_Field.thy	Fri Apr 17 22:59:19 2015 +0200
+++ b/src/HOL/Archimedean_Field.thy	Fri Apr 17 19:49:40 2015 +0200
@@ -311,7 +311,7 @@
 
 lemma floor_divide_of_int_eq:
   fixes k l :: int
-  shows "\<lfloor>of_int k / of_int l\<rfloor> = of_int (k div l)"
+  shows "\<lfloor>of_int k / of_int l\<rfloor> = k div l"
 proof (cases "l = 0")
   case True then show ?thesis by simp
 next
@@ -340,7 +340,7 @@
     by simp
   then have "\<lfloor>of_int k / of_int l :: 'a\<rfloor> = \<lfloor>of_int (k mod l) / of_int l + of_int (k div l) :: 'a\<rfloor>"
     by (simp add: ac_simps)
-  then have "\<lfloor>of_int k / of_int l :: 'a\<rfloor> = \<lfloor>of_int (k mod l) / of_int l :: 'a\<rfloor> + of_int (k div l)"
+  then have "\<lfloor>of_int k / of_int l :: 'a\<rfloor> = \<lfloor>of_int (k mod l) / of_int l :: 'a\<rfloor> + k div l"
     by simp
   with * show ?thesis by simp
 qed