src/HOL/Number_Theory/Residues.thy
changeset 50027 7747a9f4c358
parent 47163 248376f8881d
child 54489 03ff4d1e6784
     1.1 --- a/src/HOL/Number_Theory/Residues.thy	Thu Nov 08 11:59:47 2012 +0100
     1.2 +++ b/src/HOL/Number_Theory/Residues.thy	Thu Nov 08 11:59:48 2012 +0100
     1.3 @@ -131,8 +131,10 @@
     1.4  lemma finite [iff]: "finite (carrier R)"
     1.5    by (subst res_carrier_eq, auto)
     1.6  
     1.7 +declare [[simproc del: finite_Collect]]
     1.8  lemma finite_Units [iff]: "finite (Units R)"
     1.9 -  by (subst res_units_eq, auto)
    1.10 +  by (subst res_units_eq) auto
    1.11 +declare [[simproc add: finite_Collect]]
    1.12  
    1.13  (* The function a -> a mod m maps the integers to the
    1.14     residue classes. The following lemmas show that this mapping