# HG changeset patch
# User wenzelm
# Date 1393780808 -3600
# Node ID 6fe16c8a647483b8c5b2226c1cb827d374fdb674
# Parent  8dd16f8dfe9954e884e769c4c3e515f043e946db
repaired document;

diff -r 8dd16f8dfe99 -r 6fe16c8a6474 src/HOL/Word/Word.thy
--- a/src/HOL/Word/Word.thy	Sun Mar 02 18:11:30 2014 +0100
+++ b/src/HOL/Word/Word.thy	Sun Mar 02 18:20:08 2014 +0100
@@ -2018,7 +2018,7 @@
   unfolding uint_nat by (simp add : unat_mod zmod_int)
 
 
-subsection {* Definition of @[text unat_arith} tactic *}
+subsection {* Definition of @{text unat_arith} tactic *}
 
 lemma unat_split:
   fixes x::"'a::len word"