src/HOL/MacLaurin.thy
changeset 61799 4cf66f21b764
parent 61609 77b453bd616f
child 61944 5d06ecfdb472
     1.1 --- a/src/HOL/MacLaurin.thy	Mon Dec 07 10:23:50 2015 +0100
     1.2 +++ b/src/HOL/MacLaurin.thy	Mon Dec 07 10:38:04 2015 +0100
     1.3 @@ -209,7 +209,7 @@
     1.4           f h = (\<Sum>m<n. diff m 0 / (fact m) * h ^ m) +
     1.5           diff n t / (fact n) * h ^ n"
     1.6  proof -
     1.7 -  txt "Transform @{text ABL'} into @{text derivative_intros} format."
     1.8 +  txt "Transform \<open>ABL'\<close> into \<open>derivative_intros\<close> format."
     1.9    note DERIV' = DERIV_chain'[OF _ DERIV[rule_format], THEN DERIV_cong]
    1.10    from assms
    1.11    have "\<exists>t>0. t < - h \<and>