--- a/src/HOL/Number_Theory/Cong.thy Sat Nov 01 11:40:55 2014 +0100
+++ b/src/HOL/Number_Theory/Cong.thy Sat Nov 01 14:20:38 2014 +0100
@@ -161,7 +161,7 @@
lemma cong_diff_nat:
assumes"[a = b] (mod m)" "[c = d] (mod m)" "(a::nat) >= c" "b >= d"
shows "[a - c = b - d] (mod m)"
- using assms by (rule cong_diff_aux_int [transferred]);
+ using assms by (rule cong_diff_aux_int [transferred])
lemma cong_mult_nat:
"[(a::nat) = b] (mod m) \<Longrightarrow> [c = d] (mod m) \<Longrightarrow> [a * c = b * d] (mod m)"