src/HOL/GCD.thy
changeset 58776 95e58e04e534
parent 58770 ae5e9b4f8daf
child 58787 af9eb5e566dd
     1.1 --- a/src/HOL/GCD.thy	Fri Oct 24 15:07:49 2014 +0200
     1.2 +++ b/src/HOL/GCD.thy	Fri Oct 24 15:07:51 2014 +0200
     1.3 @@ -1049,7 +1049,7 @@
     1.4        apply (subst mod_div_equality [of m n, symmetric])
     1.5        (* applying simp here undoes the last substitution!
     1.6           what is procedure cancel_div_mod? *)
     1.7 -      apply (simp only: field_simps of_nat_add of_nat_mult)
     1.8 +      apply (simp only: NO_MATCH_def field_simps of_nat_add of_nat_mult)
     1.9        done
    1.10  qed
    1.11