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