# HG changeset patch
# User haftmann
# Date 1197364989 -3600
# Node ID 137ebc0603f41035044bff62ce5fe04399c1b644
# Parent  24567e50ebcc303ae101dcf120596aa167106e64
moved lemma odd_pos to theory Parity

diff -r 24567e50ebcc -r 137ebc0603f4 src/HOL/Hyperreal/NthRoot.thy
--- 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])