Mercurial Mercurial > repos > isabelle / changeset
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | raw | gz | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
less ambiguous syntax;
authorwenzelm
Mon, 19 Sep 2011 23:24:32 +0200
changeset 45006 11a542f50fc3
parent 45005 0d2d59525912
child 45007 cc86edb97c2c
less ambiguous syntax;
src/HOL/Algebra/AbelCoset.thy file | annotate | diff | comparison | revisions 
--- a/src/HOL/Algebra/AbelCoset.thy	Mon Sep 19 23:18:18 2011 +0200
+++ b/src/HOL/Algebra/AbelCoset.thy	Mon Sep 19 23:24:32 2011 +0200
@@ -36,7 +36,7 @@
   where "A_SET_INV G H = SET_INV \<lparr>carrier = carrier G, mult = add G, one = zero G\<rparr> H"
 
 definition
-  a_r_congruent :: "[('a,'b)ring_scheme, 'a set] \<Rightarrow> ('a*'a)set"  ("racong\<index> _")
+  a_r_congruent :: "[('a,'b)ring_scheme, 'a set] \<Rightarrow> ('a*'a)set"  ("racong\<index>")
   where "a_r_congruent G = r_congruent \<lparr>carrier = carrier G, mult = add G, one = zero G\<rparr>"
 
 definition
isabelle