src/HOL/Old_Number_Theory/EulerFermat.thy
changeset 45480 a39bb6d42ace
parent 44766 d4d33a4d7548
child 45605 a89b4bc311a5
     1.1 --- a/src/HOL/Old_Number_Theory/EulerFermat.thy	Sat Nov 12 21:10:56 2011 +0100
     1.2 +++ b/src/HOL/Old_Number_Theory/EulerFermat.thy	Sun Nov 13 19:26:53 2011 +0100
     1.3 @@ -142,7 +142,7 @@
     1.4      prefer 2
     1.5      apply (subst zdvd_iff_zgcd [symmetric])
     1.6       apply (rule_tac [4] zgcd_zcong_zgcd)
     1.7 -       apply (simp_all add: zcong_sym)
     1.8 +       apply (simp_all (no_asm_use) add: zcong_sym)
     1.9    done
    1.10  
    1.11