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