src/HOL/Number_Theory/Cong.thy
changeset 58860 fee7cfa69c50
parent 58623 2db1df2c8467
child 58889 5b7a9633cfa8
--- 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)"