src/HOL/Ring_and_Field.thy
changeset 23400 a64b39e5809b
parent 23398 0b5a400c7595
child 23406 167b53019d6f
     1.1 --- a/src/HOL/Ring_and_Field.thy	Fri Jun 15 19:19:23 2007 +0200
     1.2 +++ b/src/HOL/Ring_and_Field.thy	Sat Jun 16 15:01:54 2007 +0200
     1.3 @@ -1042,13 +1042,14 @@
     1.4  
     1.5  subsubsection{*Special Cancellation Simprules for Division*}
     1.6  
     1.7 -lemma mult_divide_cancel_left_if [simp]:
     1.8 +(* FIXME need not be a simp-rule once "divide_cancel_factor" has been fixed *)
     1.9 +lemma mult_divide_cancel_left_if[simp]:
    1.10    fixes c :: "'a :: {field,division_by_zero}"
    1.11    shows "(c*a) / (c*b) = (if c=0 then 0 else a/b)"
    1.12  by (simp add: mult_divide_cancel_left)
    1.13 -(* also used at ML level *)
    1.14  
    1.15 -lemma mult_divide_cancel_right_if [simp]:
    1.16 +(* Not needed anymore because now subsumed by simproc "divide_cancel_factor"
    1.17 +lemma mult_divide_cancel_right_if:
    1.18    fixes c :: "'a :: {field,division_by_zero}"
    1.19    shows "(a*c) / (b*c) = (if c=0 then 0 else a/b)"
    1.20  by (simp add: mult_divide_cancel_right)
    1.21 @@ -1092,7 +1093,7 @@
    1.22    fixes a :: "'a :: {field,division_by_zero}"
    1.23    shows "(b/a) * a = (if a=0 then 0 else b)"
    1.24  by (simp add: times_divide_eq_left)
    1.25 -
    1.26 +*)
    1.27  
    1.28  subsection {* Division and Unary Minus *}
    1.29