src/HOL/Real_Vector_Spaces.thy
changeset 62131 1baed43f453e
parent 62102 877463945ce9
child 62347 2230b7047376
     1.1 --- a/src/HOL/Real_Vector_Spaces.thy	Mon Jan 11 16:38:39 2016 +0100
     1.2 +++ b/src/HOL/Real_Vector_Spaces.thy	Mon Jan 11 22:14:15 2016 +0000
     1.3 @@ -313,8 +313,7 @@
     1.4  by (simp add: divide_inverse nonzero_of_real_inverse)
     1.5  
     1.6  lemma of_real_divide [simp]:
     1.7 -  "of_real (x / y) =
     1.8 -   (of_real x / of_real y :: 'a::{real_field, field})"
     1.9 +  "of_real (x / y) = (of_real x / of_real y :: 'a::real_div_algebra)"
    1.10  by (simp add: divide_inverse)
    1.11  
    1.12  lemma of_real_power [simp]: