# HG changeset patch
# User wenzelm
# Date 1314220780 -7200
# Node ID 3c2b2c4a7c1cb15daa1484a71e887bac286e526e
# Parent  6c6c31ef6bb24efe8150772e744149c0819388a7
tuned syntax -- avoid ambiguities;

diff -r 6c6c31ef6bb2 -r 3c2b2c4a7c1c src/HOL/Algebra/Congruence.thy
--- a/src/HOL/Algebra/Congruence.thy	Wed Aug 24 23:00:53 2011 +0200
+++ b/src/HOL/Algebra/Congruence.thy	Wed Aug 24 23:19:40 2011 +0200
@@ -29,15 +29,15 @@
   where "A {.=}\<^bsub>S\<^esub> B \<longleftrightarrow> ((\<forall>x \<in> A. x .\<in>\<^bsub>S\<^esub> B) \<and> (\<forall>x \<in> B. x .\<in>\<^bsub>S\<^esub> A))"
 
 definition
-  eq_class_of :: "_ \<Rightarrow> 'a \<Rightarrow> 'a set" ("class'_of\<index> _")
+  eq_class_of :: "_ \<Rightarrow> 'a \<Rightarrow> 'a set" ("class'_of\<index>")
   where "class_of\<^bsub>S\<^esub> x = {y \<in> carrier S. x .=\<^bsub>S\<^esub> y}"
 
 definition
-  eq_closure_of :: "_ \<Rightarrow> 'a set \<Rightarrow> 'a set" ("closure'_of\<index> _")
+  eq_closure_of :: "_ \<Rightarrow> 'a set \<Rightarrow> 'a set" ("closure'_of\<index>")
   where "closure_of\<^bsub>S\<^esub> A = {y \<in> carrier S. y .\<in>\<^bsub>S\<^esub> A}"
 
 definition
-  eq_is_closed :: "_ \<Rightarrow> 'a set \<Rightarrow> bool" ("is'_closed\<index> _")
+  eq_is_closed :: "_ \<Rightarrow> 'a set \<Rightarrow> bool" ("is'_closed\<index>")
   where "is_closed\<^bsub>S\<^esub> A \<longleftrightarrow> A \<subseteq> carrier S \<and> closure_of\<^bsub>S\<^esub> A = A"
 
 abbreviation