src/HOL/Hyperreal/NthRoot.thy
changeset 23441 ee218296d635
parent 23257 9117e228a8e3
child 23475 c869b52a9077
     1.1 --- a/src/HOL/Hyperreal/NthRoot.thy	Wed Jun 20 17:34:44 2007 +0200
     1.2 +++ b/src/HOL/Hyperreal/NthRoot.thy	Wed Jun 20 19:49:14 2007 +0200
     1.3 @@ -355,7 +355,7 @@
     1.4    show "real n * root n x ^ (n - Suc 0) \<noteq> 0"
     1.5      using n x by simp
     1.6    show "isCont (root n) x"
     1.7 -    by (rule isCont_real_root)
     1.8 +    using n by (rule isCont_real_root)
     1.9  qed
    1.10  
    1.11  lemma DERIV_odd_real_root: