# HG changeset patch
# User paulson
# Date 978948384 -3600
# Node ID 47c4a76b0c7aa771cf97a67bd7cad3c206eff3b0
# Parent  4a212e635318f138c8c686086afcd7e25287deeb
additional pattern allows reduction of fractions to lowest terms

diff -r 4a212e635318 -r 47c4a76b0c7a src/HOL/Hyperreal/HyperArith0.ML
--- 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 = 
diff -r 4a212e635318 -r 47c4a76b0c7a src/HOL/Real/RealArith0.ML
--- 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 =