Mercurial Mercurial > repos > isabelle / changeset
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | raw | gz | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
use {less,le}_number_of in integer simprocs
authorhuffman
Tue, 09 Dec 2008 20:35:31 -0800
changeset 29038 90f42c138585
parent 29037 208fee4049a0
child 29039 8b9207f82a78
use {less,le}_number_of in integer simprocs
src/HOL/Tools/int_factor_simprocs.ML file | annotate | diff | comparison | revisions 
--- a/src/HOL/Tools/int_factor_simprocs.ML	Tue Dec 09 16:26:47 2008 -0800
+++ b/src/HOL/Tools/int_factor_simprocs.ML	Tue Dec 09 20:35:31 2008 -0800
@@ -19,7 +19,7 @@
 and d = gcd(m,m') and n=m/d and n'=m'/d.
 *)
 
-val rel_number_of = [@{thm eq_number_of_eq}, @{thm less_number_of_eq_neg}, @{thm le_number_of_eq}];
+val rel_number_of = [@{thm eq_number_of_eq}, @{thm less_number_of}, @{thm le_number_of}];
 
 local
   open Int_Numeral_Simprocs
isabelle