moved lemma odd_pos to theory Parity
authorhaftmann
Tue Dec 11 10:23:09 2007 +0100 (2007-12-11)
changeset 25602137ebc0603f4
parent 25601 24567e50ebcc
child 25603 4b7a58fc168c
moved lemma odd_pos to theory Parity
src/HOL/Hyperreal/NthRoot.thy
     1.1 --- a/src/HOL/Hyperreal/NthRoot.thy	Tue Dec 11 10:23:08 2007 +0100
     1.2 +++ b/src/HOL/Hyperreal/NthRoot.thy	Tue Dec 11 10:23:09 2007 +0100
     1.3 @@ -7,7 +7,7 @@
     1.4  header {* Nth Roots of Real Numbers *}
     1.5  
     1.6  theory NthRoot
     1.7 -imports SEQ Parity Deriv
     1.8 +imports Parity "../Hyperreal/Deriv"
     1.9  begin
    1.10  
    1.11  subsection {* Existence of Nth Root *}
    1.12 @@ -83,9 +83,6 @@
    1.13    "\<lbrakk>0 < n; 0 \<le> x\<rbrakk> \<Longrightarrow> root n x ^ n = x"
    1.14  by (auto simp add: order_le_less real_root_pow_pos)
    1.15  
    1.16 -lemma odd_pos: "odd (n::nat) \<Longrightarrow> 0 < n"
    1.17 -by (cases n, simp_all)
    1.18 -
    1.19  lemma odd_real_root_pow: "odd n \<Longrightarrow> root n x ^ n = x"
    1.20  apply (rule_tac x=0 and y=x in linorder_le_cases)
    1.21  apply (erule (1) real_root_pow_pos2 [OF odd_pos])