# HG changeset patch
# User nipkow
# Date 1393782101 -3600
# Node ID eb8e231a335fe136c88f14717609911cfd143b1e
# Parent  6fe16c8a647483b8c5b2226c1cb827d374fdb674# Parent  459b5561ba4e7670adacf0b63f258565c5d59aae
merged

diff -r 459b5561ba4e -r eb8e231a335f src/HOL/Transcendental.thy
--- 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]
diff -r 459b5561ba4e -r eb8e231a335f src/HOL/Word/Word.thy
--- 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"