--- a/src/HOL/Number_Theory/Residues.thy Thu Nov 28 22:03:41 2013 +0100
+++ b/src/HOL/Number_Theory/Residues.thy Fri Nov 29 08:26:45 2013 +0100
@@ -131,10 +131,8 @@
lemma finite [iff]: "finite (carrier R)"
by (subst res_carrier_eq, auto)
-declare [[simproc del: finite_Collect]]
lemma finite_Units [iff]: "finite (Units R)"
by (subst res_units_eq) auto
-declare [[simproc add: finite_Collect]]
(* The function a -> a mod m maps the integers to the
residue classes. The following lemmas show that this mapping