src/HOL/Number_Theory/Cong.thy
changeset 58937 49e8115f70d8
parent 58889 5b7a9633cfa8
child 59010 ec2b4270a502
     1.1 --- a/src/HOL/Number_Theory/Cong.thy	Fri Nov 07 22:15:51 2014 +0100
     1.2 +++ b/src/HOL/Number_Theory/Cong.thy	Fri Nov 07 22:33:54 2014 +0100
     1.3 @@ -40,10 +40,10 @@
     1.4  subsection {* Main definitions *}
     1.5  
     1.6  class cong =
     1.7 -  fixes cong :: "'a \<Rightarrow> 'a \<Rightarrow> 'a \<Rightarrow> bool" ("(1[_ = _] '(mod _'))")
     1.8 +  fixes cong :: "'a \<Rightarrow> 'a \<Rightarrow> 'a \<Rightarrow> bool" ("(1[_ = _] '(()mod _'))")
     1.9  begin
    1.10  
    1.11 -abbreviation notcong :: "'a \<Rightarrow> 'a \<Rightarrow> 'a \<Rightarrow> bool"  ("(1[_ \<noteq> _] '(mod _'))")
    1.12 +abbreviation notcong :: "'a \<Rightarrow> 'a \<Rightarrow> 'a \<Rightarrow> bool"  ("(1[_ \<noteq> _] '(()mod _'))")
    1.13    where "notcong x y m \<equiv> \<not> cong x y m"
    1.14  
    1.15  end