changeset 29038 | 90f42c138585 |
parent 28952 | 15a4b2cf8c34 |
child 29981 | 7d0ed261b712 |
child 30240 | 5b25fee0362c |
--- 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