src/HOL/NumberTheory/EulerFermat.thy
changeset 14174 f3cafd2929d5
parent 13833 f8dcb1d9ea68
child 15003 6145dd7538d7
     1.1 --- a/src/HOL/NumberTheory/EulerFermat.thy	Fri Aug 29 13:18:45 2003 +0200
     1.2 +++ b/src/HOL/NumberTheory/EulerFermat.thy	Fri Aug 29 15:19:02 2003 +0200
     1.3 @@ -145,7 +145,7 @@
     1.4     apply (rule_tac [2] m = m in zcong_zless_imp_eq)
     1.5         apply (auto intro: Bnor_mem_zle Bnor_mem_zg zcong_trans
     1.6  	 order_less_imp_le norR_mem_unique_aux simp add: zcong_sym)
     1.7 -  apply (rule_tac "x" = b in exI, safe)
     1.8 +  apply (rule_tac x = b in exI, safe)
     1.9    apply (rule Bnor_mem_if)
    1.10      apply (case_tac [2] "b = 0")
    1.11       apply (auto intro: order_less_le [THEN iffD2])