Mercurial Mercurial > repos > isabelle / diff
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | file | latest | revisions | annotate | diff | comparison | raw | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
src/HOL/NSA/HSeries.thy
changeset 61982 3af5a06577c7
parent 61981 1b5845c62fa0 
--- a/src/HOL/NSA/HSeries.thy	Wed Dec 30 17:55:43 2015 +0100
+++ b/src/HOL/NSA/HSeries.thy	Wed Dec 30 18:03:23 2015 +0100
@@ -129,8 +129,8 @@
 lemma starfunNat_sumr: "!!N. ( *f* (%n. setsum f {0..<n})) N = sumhr(0,N,f)"
 unfolding sumhr_app by transfer (rule refl)
 
-lemma sumhr_hrabs_approx [simp]: "sumhr(0, M, f) @= sumhr(0, N, f)
-      ==> \<bar>sumhr(M, N, f)\<bar> @= 0"
+lemma sumhr_hrabs_approx [simp]: "sumhr(0, M, f) \<approx> sumhr(0, N, f)
+      ==> \<bar>sumhr(M, N, f)\<bar> \<approx> 0"
 apply (cut_tac x = M and y = N in linorder_less_linear)
 apply (auto simp add: approx_refl)
 apply (drule approx_sym [THEN approx_minus_iff [THEN iffD1]])
@@ -167,7 +167,7 @@
 
 lemma NSsummable_NSCauchy:
      "NSsummable f =
-      (\<forall>M \<in> HNatInfinite. \<forall>N \<in> HNatInfinite. \<bar>sumhr(M,N,f)\<bar> @= 0)"
+      (\<forall>M \<in> HNatInfinite. \<forall>N \<in> HNatInfinite. \<bar>sumhr(M,N,f)\<bar> \<approx> 0)"
 apply (auto simp add: summable_NSsummable_iff [symmetric]
        summable_iff_convergent convergent_NSconvergent_iff atLeast0LessThan[symmetric]
        NSCauchy_NSconvergent_iff [symmetric] NSCauchy_def starfunNat_sumr)
isabelle