Mercurial Mercurial > repos > isabelle / changeset
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | raw | gz | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
tuned proof
authorhaftmann
Tue, 23 Oct 2007 11:48:10 +0200
changeset 25153 af3c7e99fed0
parent 25152 bfde2f8c0f63
child 25154 6155f2faf23e
tuned proof
src/HOL/Hyperreal/Transcendental.thy file | annotate | diff | comparison | revisions 
--- a/src/HOL/Hyperreal/Transcendental.thy	Tue Oct 23 11:48:08 2007 +0200
+++ b/src/HOL/Hyperreal/Transcendental.thy	Tue Oct 23 11:48:10 2007 +0200
@@ -33,7 +33,7 @@
   fixes y :: "'a::{recpower,comm_ring}" shows
      "x ^ (Suc n) - y ^ (Suc n) =  
       (x - y) * (\<Sum>p=0..<Suc n. (x ^ p) * y ^ (n - p))"
-apply (induct "n", simp add: power_Suc)
+apply (induct n, simp add: power_Suc)
 apply (simp add: power_Suc del: setsum_op_ivl_Suc)
 apply (subst setsum_op_ivl_Suc)
 apply (subst lemma_realpow_diff_sumr)
isabelle