src/HOL/Word/Word.thy
changeset 55833 6fe16c8a6474
parent 55818 d8b2f50705d0
child 55945 e96383acecf9
     1.1 --- a/src/HOL/Word/Word.thy	Sun Mar 02 18:11:30 2014 +0100
     1.2 +++ b/src/HOL/Word/Word.thy	Sun Mar 02 18:20:08 2014 +0100
     1.3 @@ -2018,7 +2018,7 @@
     1.4    unfolding uint_nat by (simp add : unat_mod zmod_int)
     1.5  
     1.6  
     1.7 -subsection {* Definition of @[text unat_arith} tactic *}
     1.8 +subsection {* Definition of @{text unat_arith} tactic *}
     1.9  
    1.10  lemma unat_split:
    1.11    fixes x::"'a::len word"