src/HOL/Hyperreal/NthRoot.thy
changeset 25602 137ebc0603f4
parent 23477 f4b83f03cac9
child 25766 6960410f134d
--- a/src/HOL/Hyperreal/NthRoot.thy	Tue Dec 11 10:23:08 2007 +0100
+++ b/src/HOL/Hyperreal/NthRoot.thy	Tue Dec 11 10:23:09 2007 +0100
@@ -7,7 +7,7 @@
 header {* Nth Roots of Real Numbers *}
 
 theory NthRoot
-imports SEQ Parity Deriv
+imports Parity "../Hyperreal/Deriv"
 begin
 
 subsection {* Existence of Nth Root *}
@@ -83,9 +83,6 @@
   "\<lbrakk>0 < n; 0 \<le> x\<rbrakk> \<Longrightarrow> root n x ^ n = x"
 by (auto simp add: order_le_less real_root_pow_pos)
 
-lemma odd_pos: "odd (n::nat) \<Longrightarrow> 0 < n"
-by (cases n, simp_all)
-
 lemma odd_real_root_pow: "odd n \<Longrightarrow> root n x ^ n = x"
 apply (rule_tac x=0 and y=x in linorder_le_cases)
 apply (erule (1) real_root_pow_pos2 [OF odd_pos])