src/HOL/NumberTheory/IntPrimes.thy
changeset 14378 69c4d5997669
parent 14353 79f9fbef9106
child 14387 e96d5c42c4b0
     1.1 --- a/src/HOL/NumberTheory/IntPrimes.thy	Thu Feb 05 10:45:28 2004 +0100
     1.2 +++ b/src/HOL/NumberTheory/IntPrimes.thy	Tue Feb 10 12:02:11 2004 +0100
     1.3 @@ -338,7 +338,7 @@
     1.4      a < m ==> 0 \<le> b ==> b < m ==> [a = b] (mod m) ==> a = b"
     1.5    apply (unfold zcong_def dvd_def, auto)
     1.6    apply (drule_tac f = "\<lambda>z. z mod m" in arg_cong)
     1.7 -  apply (cut_tac z = a and w = b in zless_linear, auto)
     1.8 +  apply (cut_tac x = a and y = b in linorder_less_linear, auto)
     1.9     apply (subgoal_tac [2] "(a - b) mod m = a - b")
    1.10      apply (rule_tac [3] mod_pos_pos_trivial, auto)
    1.11    apply (subgoal_tac "(m + (a - b)) mod m = m + (a - b)")