Mercurial Mercurial > repos > isabelle / diff
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | file | latest | revisions | annotate | diff | comparison | raw | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
src/HOL/Real/real_arith.ML
changeset 14336 8f731d3cd65b
parent 14334 6137d24eef79
child 14352 a8b1a44d8264 
--- a/src/HOL/Real/real_arith.ML	Thu Jan 01 21:47:07 2004 +0100
+++ b/src/HOL/Real/real_arith.ML	Sat Jan 03 16:09:39 2004 +0100
@@ -217,8 +217,7 @@
              inst "a" "(number_of ?v)::real" right_distrib,
              divide_1,times_divide_eq_right,times_divide_eq_left];
 
-val simprocs = [real_cancel_numeral_factors_divide,
-                real_cancel_numeral_factors_divide];
+val simprocs = [real_cancel_numeral_factors_divide];
 
 fun cvar(th,_ $ (_ $ _ $ var)) = cterm_of (#sign(rep_thm th)) var;
isabelle