src/HOL/Old_Number_Theory/EulerFermat.thy
changeset 45480 a39bb6d42ace
parent 44766 d4d33a4d7548
child 45605 a89b4bc311a5
equal deleted inserted replaced
45477:11d9c2768729 45480:a39bb6d42ace
   140    apply (simp only: zcong_def)
   140    apply (simp only: zcong_def)
   141    apply (subgoal_tac "zgcd a m = m")
   141    apply (subgoal_tac "zgcd a m = m")
   142     prefer 2
   142     prefer 2
   143     apply (subst zdvd_iff_zgcd [symmetric])
   143     apply (subst zdvd_iff_zgcd [symmetric])
   144      apply (rule_tac [4] zgcd_zcong_zgcd)
   144      apply (rule_tac [4] zgcd_zcong_zgcd)
   145        apply (simp_all add: zcong_sym)
   145        apply (simp_all (no_asm_use) add: zcong_sym)
   146   done
   146   done
   147 
   147 
   148 
   148 
   149 text {* \medskip @{term noXRRset} *}
   149 text {* \medskip @{term noXRRset} *}
   150 
   150