repaired document;
authorwenzelm
Sun Mar 02 18:11:30 2014 +0100 (2014-03-02)
changeset 558328dd16f8dfe99
parent 55831 3a9386b32211
child 55833 6fe16c8a6474
repaired document;
src/HOL/Transcendental.thy
     1.1 --- a/src/HOL/Transcendental.thy	Sun Mar 02 00:05:35 2014 +0100
     1.2 +++ b/src/HOL/Transcendental.thy	Sun Mar 02 18:11:30 2014 +0100
     1.3 @@ -52,7 +52,7 @@
     1.4    finally show ?case .
     1.5  qed
     1.6  
     1.7 -corollary power_diff_sumr2: --{*COMPLEX_POLYFUN in HOL Light*}
     1.8 +corollary power_diff_sumr2: --{* @{text COMPLEX_POLYFUN} in HOL Light *}
     1.9    fixes x :: "'a::{comm_ring,monoid_mult}"
    1.10    shows   "x^n - y^n = (x - y) * (\<Sum>i=0..<n. y^(n - Suc i) * x^i)"
    1.11  using lemma_realpow_diff_sumr2[of x "n - 1" y]