--- a/src/HOL/Number_Theory/Cong.thy Fri Nov 07 22:15:51 2014 +0100
+++ b/src/HOL/Number_Theory/Cong.thy Fri Nov 07 22:33:54 2014 +0100
@@ -40,10 +40,10 @@
subsection {* Main definitions *}
class cong =
- fixes cong :: "'a \<Rightarrow> 'a \<Rightarrow> 'a \<Rightarrow> bool" ("(1[_ = _] '(mod _'))")
+ fixes cong :: "'a \<Rightarrow> 'a \<Rightarrow> 'a \<Rightarrow> bool" ("(1[_ = _] '(()mod _'))")
begin
-abbreviation notcong :: "'a \<Rightarrow> 'a \<Rightarrow> 'a \<Rightarrow> bool" ("(1[_ \<noteq> _] '(mod _'))")
+abbreviation notcong :: "'a \<Rightarrow> 'a \<Rightarrow> 'a \<Rightarrow> bool" ("(1[_ \<noteq> _] '(()mod _'))")
where "notcong x y m \<equiv> \<not> cong x y m"
end