merged
authornipkow
Sun, 02 Mar 2014 18:41:41 +0100
changeset 55835 eb8e231a335f
parent 55833 6fe16c8a6474 (diff)
parent 55834 459b5561ba4e (current diff)
child 55836 8093590e49e4
child 55837 154855d9a564
merged
--- 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"