src/HOL/Rat.thy
changeset 56479 91958d4b30f7
parent 56409 36489d77c484
child 56544 b60d5d119489
     1.1 --- a/src/HOL/Rat.thy	Tue Apr 08 23:16:00 2014 +0200
     1.2 +++ b/src/HOL/Rat.thy	Wed Apr 09 09:37:47 2014 +0200
     1.3 @@ -665,7 +665,7 @@
     1.4    by transfer (simp add: add_frac_eq)
     1.5  
     1.6  lemma of_rat_minus: "of_rat (- a) = - of_rat a"
     1.7 -  by transfer (simp add: divide_minus_left)
     1.8 +  by transfer simp
     1.9  
    1.10  lemma of_rat_neg_one [simp]:
    1.11    "of_rat (- 1) = - 1"