src/HOL/MacLaurin.thy
changeset 67091 1393c2340eec
parent 65273 917ae0ba03a2
child 68157 057d5b4ce47e
     1.1 --- a/src/HOL/MacLaurin.thy	Sun Nov 26 13:19:52 2017 +0100
     1.2 +++ b/src/HOL/MacLaurin.thy	Sun Nov 26 21:08:32 2017 +0100
     1.3 @@ -209,7 +209,7 @@
     1.4    fixes n :: nat and h :: real
     1.5    shows
     1.6      "h < 0 \<and> n > 0 \<and> diff 0 = f \<and>
     1.7 -      (\<forall>m t. m < n & h \<le> t & t \<le> 0 --> DERIV (diff m) t :> diff (Suc m) t) \<longrightarrow>
     1.8 +      (\<forall>m t. m < n \<and> h \<le> t \<and> t \<le> 0 \<longrightarrow> DERIV (diff m) t :> diff (Suc m) t) \<longrightarrow>
     1.9      (\<exists>t. h < t \<and> t < 0 \<and> f h = (\<Sum>m<n. diff m 0 / fact m * h ^ m) + diff n t / fact n * h ^ n)"
    1.10    by (blast intro: Maclaurin_minus)
    1.11  
    1.12 @@ -373,7 +373,7 @@
    1.13  
    1.14  subsection \<open>Version for Sine Function\<close>
    1.15  
    1.16 -lemma mod_exhaust_less_4: "m mod 4 = 0 | m mod 4 = 1 | m mod 4 = 2 | m mod 4 = 3"
    1.17 +lemma mod_exhaust_less_4: "m mod 4 = 0 \<or> m mod 4 = 1 \<or> m mod 4 = 2 \<or> m mod 4 = 3"
    1.18    for m :: nat
    1.19    by auto
    1.20