# HG changeset patch
# User wenzelm
# Date 1393780290 -3600
# Node ID 8dd16f8dfe9954e884e769c4c3e515f043e946db
# Parent  3a9386b32211c9b2027add8dc7b3ded65bf3126c
repaired document;

diff -r 3a9386b32211 -r 8dd16f8dfe99 src/HOL/Transcendental.thy
--- a/src/HOL/Transcendental.thy	Sun Mar 02 00:05:35 2014 +0100
+++ b/src/HOL/Transcendental.thy	Sun Mar 02 18:11:30 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]