src/HOL/Deriv.thy
changeset 29987 391dcbd7e4dd
parent 29985 57975b45ab70
child 30242 aea5d7fa7ef5
     1.1 --- a/src/HOL/Deriv.thy	Wed Feb 18 19:51:39 2009 -0800
     1.2 +++ b/src/HOL/Deriv.thy	Wed Feb 18 20:14:45 2009 -0800
     1.3 @@ -9,7 +9,7 @@
     1.4  header{* Differentiation *}
     1.5  
     1.6  theory Deriv
     1.7 -imports Lim Polynomial
     1.8 +imports Lim
     1.9  begin
    1.10  
    1.11  text{*Standard Definitions*}