src/HOL/Library/Pocklington.thy
changeset 30042 31039ee583fa
parent 29667 53103fc8ffa3
child 30224 79136ce06bdb
     1.1 --- a/src/HOL/Library/Pocklington.thy	Sat Feb 21 09:58:45 2009 +0100
     1.2 +++ b/src/HOL/Library/Pocklington.thy	Sat Feb 21 20:52:30 2009 +0100
     1.3 @@ -873,7 +873,7 @@
     1.4        from lh[unfolded nat_mod] 
     1.5        obtain q1 q2 where q12:"a ^ d + n * q1 = 1 + n * q2" by blast
     1.6        hence "a ^ d + n * q1 - n * q2 = 1" by simp
     1.7 -      with dvd_diff [OF dvd_add [OF divides_rexp[OF p(2), of d'] dvd_mult2[OF p(1), of q1]] dvd_mult2[OF p(1), of q2]] d' have "p dvd 1" by simp 
     1.8 +      with nat_dvd_diff [OF dvd_add [OF divides_rexp[OF p(2), of d'] dvd_mult2[OF p(1), of q1]] dvd_mult2[OF p(1), of q2]] d' have "p dvd 1" by simp
     1.9        with p(3) have False by simp
    1.10        hence ?rhs ..}
    1.11      ultimately have ?rhs by blast}