src/HOL/Library/Abstract_Rat.thy
changeset 29667 53103fc8ffa3
parent 28615 4c8fa015ec7f
child 30042 31039ee583fa
     1.1 --- a/src/HOL/Library/Abstract_Rat.thy	Sun Jan 18 13:58:17 2009 +0100
     1.2 +++ b/src/HOL/Library/Abstract_Rat.thy	Wed Jan 28 16:29:16 2009 +0100
     1.3 @@ -240,7 +240,7 @@
     1.4      by (simp only: of_int_mult[symmetric] of_int_add [symmetric])
     1.5    then have "of_int x / of_int d = ?t / of_int d" 
     1.6      using cong[OF refl[of ?f] eq] by simp
     1.7 -  then show ?thesis by (simp add: add_divide_distrib ring_simps prems)
     1.8 +  then show ?thesis by (simp add: add_divide_distrib algebra_simps prems)
     1.9  qed
    1.10  
    1.11  lemma of_int_div: "(d::int) ~= 0 ==> d dvd n ==>