| changeset 55833 | 6fe16c8a6474 |
| parent 55818 | d8b2f50705d0 |
| child 55945 | e96383acecf9 |
--- 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"