src/HOL/Algebra/QuotRing.thy
changeset 21502 7f3ea2b3bab6
parent 20318 0e0ea63fe768
child 23350 50c5b0912a0c
--- a/src/HOL/Algebra/QuotRing.thy	Thu Nov 23 20:33:42 2006 +0100
+++ b/src/HOL/Algebra/QuotRing.thy	Thu Nov 23 20:34:21 2006 +0100
@@ -114,7 +114,7 @@
       --{* mult closed *}
       apply (clarify)
       apply (simp add: rcoset_mult_add, fast)
-     --{* mult one\_closed *}
+     --{* mult @{text one_closed} *}
      apply (force intro: one_closed)
     --{* mult assoc *}
     apply clarify