additional pattern allows reduction of fractions to lowest terms

--- a/src/HOL/Hyperreal/HyperArith0.ML	Mon Jan 08 10:33:51 2001 +0100
+++ b/src/HOL/Hyperreal/HyperArith0.ML	Mon Jan 08 11:06:24 2001 +0100
@@ -269,7 +269,8 @@
 
 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 = 

--- a/src/HOL/Real/RealArith0.ML	Mon Jan 08 10:33:51 2001 +0100
+++ b/src/HOL/Real/RealArith0.ML	Mon Jan 08 11:06:24 2001 +0100
@@ -257,7 +257,8 @@
 
 val real_cancel_numeral_factors_divide = prep_simproc
 	("realdiv_cancel_numeral_factor", 
-	 prep_pats ["((l::real) * m) / n", "(l::real) / (m * n)"], 
+	 prep_pats ["((l::real) * m) / n", "(l::real) / (m * n)", 
+                     "((number_of v)::real) / (number_of w)"], 
 	 DivCancelNumeralFactor.proc);
 
 val real_cancel_numeral_factors =