src/HOL/Ring_and_Field.thy
changeset 22993 838c66e760b5
parent 22990 775e9de3db48
child 23073 d810dc04b96d
     1.1 --- a/src/HOL/Ring_and_Field.thy	Thu May 17 19:29:39 2007 +0200
     1.2 +++ b/src/HOL/Ring_and_Field.thy	Thu May 17 19:49:16 2007 +0200
     1.3 @@ -932,16 +932,18 @@
     1.4       "inverse(a*b) = inverse(a) * inverse(b::'a::{field,division_by_zero})"
     1.5    proof cases
     1.6      assume "a \<noteq> 0 & b \<noteq> 0" 
     1.7 -    thus ?thesis  by (simp add: nonzero_inverse_mult_distrib mult_commute)
     1.8 +    thus ?thesis
     1.9 +      by (simp add: nonzero_inverse_mult_distrib mult_commute)
    1.10    next
    1.11      assume "~ (a \<noteq> 0 & b \<noteq> 0)" 
    1.12 -    thus ?thesis  by force
    1.13 +    thus ?thesis
    1.14 +      by force
    1.15    qed
    1.16  
    1.17  lemma division_ring_inverse_add:
    1.18    "[|(a::'a::division_ring) \<noteq> 0; b \<noteq> 0|]
    1.19     ==> inverse a + inverse b = inverse a * (a+b) * inverse b"
    1.20 -by (simp add: right_distrib left_distrib mult_assoc)
    1.21 +  by (simp add: right_distrib left_distrib mult_assoc)
    1.22  
    1.23  lemma division_ring_inverse_diff:
    1.24    "[|(a::'a::division_ring) \<noteq> 0; b \<noteq> 0|]