# HG changeset patch
# User wenzelm
# Date 1415396034 -3600
# Node ID 49e8115f70d854ffc1ceaa755e99f3d0b37ab260
# Parent  7fbe4436952d355d267755e981fd49a48bda17e7
tuned syntax -- separate tokens;

diff -r 7fbe4436952d -r 49e8115f70d8 src/HOL/Number_Theory/Cong.thy
--- 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