src/HOL/Hyperreal/HyperArith0.ML

      prep_pats ["(l::hypreal) * m <= n", "(l::hypreal) <= m * n"], 
      LeCancelNumeralFactor.proc)];
 
 val hypreal_cancel_numeral_factors_divide = prep_simproc
 	("hyprealdiv_cancel_numeral_factor", 
-	 prep_pats ["((l::hypreal) * m) / n", "(l::hypreal) / (m * n)"], 
+	 prep_pats ["((l::hypreal) * m) / n", "(l::hypreal) / (m * n)", 
+                     "((number_of v)::hypreal) / (number_of w)"], 
 	 DivCancelNumeralFactor.proc);
 
 val hypreal_cancel_numeral_factors = 
     hypreal_cancel_numeral_factors_relations @ 
     [hypreal_cancel_numeral_factors_divide];