--- a/src/HOL/Transcendental.thy Sun Mar 02 18:41:26 2014 +0100
+++ b/src/HOL/Transcendental.thy Sun Mar 02 18:41:41 2014 +0100
@@ -52,7 +52,7 @@
finally show ?case .
qed
-corollary power_diff_sumr2: --{*COMPLEX_POLYFUN in HOL Light*}
+corollary power_diff_sumr2: --{* @{text COMPLEX_POLYFUN} in HOL Light *}
fixes x :: "'a::{comm_ring,monoid_mult}"
shows "x^n - y^n = (x - y) * (\<Sum>i=0..<n. y^(n - Suc i) * x^i)"
using lemma_realpow_diff_sumr2[of x "n - 1" y]
--- a/src/HOL/Word/Word.thy Sun Mar 02 18:41:26 2014 +0100
+++ b/src/HOL/Word/Word.thy Sun Mar 02 18:41:41 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"