src/HOL/NthRoot.thy
changeset 58770 ae5e9b4f8daf
parent 58709 efdc6c533bd3
child 58889 5b7a9633cfa8
     1.1 --- a/src/HOL/NthRoot.thy	Thu Oct 23 14:04:05 2014 +0200
     1.2 +++ b/src/HOL/NthRoot.thy	Thu Oct 23 14:04:05 2014 +0200
     1.3 @@ -7,7 +7,7 @@
     1.4  header {* Nth Roots of Real Numbers *}
     1.5  
     1.6  theory NthRoot
     1.7 -imports Parity Deriv
     1.8 +imports Deriv
     1.9  begin
    1.10  
    1.11  lemma abs_sgn_eq: "abs (sgn x :: real) = (if x = 0 then 0 else 1)"