less ambiguous syntax;
authorwenzelm
Mon Sep 19 23:24:32 2011 +0200 (2011-09-19)
changeset 4500611a542f50fc3
parent 45005 0d2d59525912
child 45007 cc86edb97c2c
less ambiguous syntax;
src/HOL/Algebra/AbelCoset.thy
     1.1 --- a/src/HOL/Algebra/AbelCoset.thy	Mon Sep 19 23:18:18 2011 +0200
     1.2 +++ b/src/HOL/Algebra/AbelCoset.thy	Mon Sep 19 23:24:32 2011 +0200
     1.3 @@ -36,7 +36,7 @@
     1.4    where "A_SET_INV G H = SET_INV \<lparr>carrier = carrier G, mult = add G, one = zero G\<rparr> H"
     1.5  
     1.6  definition
     1.7 -  a_r_congruent :: "[('a,'b)ring_scheme, 'a set] \<Rightarrow> ('a*'a)set"  ("racong\<index> _")
     1.8 +  a_r_congruent :: "[('a,'b)ring_scheme, 'a set] \<Rightarrow> ('a*'a)set"  ("racong\<index>")
     1.9    where "a_r_congruent G = r_congruent \<lparr>carrier = carrier G, mult = add G, one = zero G\<rparr>"
    1.10  
    1.11  definition