src/HOL/Deriv.thy
changeset 31902 862ae16a799d
parent 31899 1a7ade46061b
child 33654 abf780db30ea
     1.1 --- a/src/HOL/Deriv.thy	Thu Jul 02 17:33:36 2009 +0200
     1.2 +++ b/src/HOL/Deriv.thy	Thu Jul 02 17:34:14 2009 +0200
     1.3 @@ -315,14 +315,14 @@
     1.4  
     1.5  text {* @{text "DERIV_intros"} *}
     1.6  ML {*
     1.7 -structure DerivIntros = NamedThmsFun
     1.8 +structure Deriv_Intros = Named_Thms
     1.9  (
    1.10    val name = "DERIV_intros"
    1.11    val description = "DERIV introduction rules"
    1.12  )
    1.13  *}
    1.14  
    1.15 -setup DerivIntros.setup
    1.16 +setup Deriv_Intros.setup
    1.17  
    1.18  lemma DERIV_cong: "\<lbrakk> DERIV f x :> X ; X = Y \<rbrakk> \<Longrightarrow> DERIV f x :> Y"
    1.19    by simp