# HG changeset patch
# User eberlm <eberlm@in.tum.de>
# Date 1501862630 -7200
# Node ID 1f66c7d77002149f9f339136e03f2e9b1292562b
# Parent  56f8bfe1211cdac8f0be259b6247a277fcb00ded# Parent  1a8441ec5cedb5d53350bc5e5d514912a74c8dd9
Merged

diff -r 1a8441ec5ced -r 1f66c7d77002 src/HOL/Computational_Algebra/Formal_Power_Series.thy
--- a/src/HOL/Computational_Algebra/Formal_Power_Series.thy	Fri Aug 04 08:13:00 2017 +0200
+++ b/src/HOL/Computational_Algebra/Formal_Power_Series.thy	Fri Aug 04 18:03:50 2017 +0200
@@ -818,8 +818,6 @@
 
 subsection \<open>Formal Power series form a metric space\<close>
 
-definition (in dist) "ball x r = {y. dist y x < r}"
-
 instantiation fps :: (comm_ring_1) dist
 begin
 
@@ -884,8 +882,8 @@
 
 declare uniformity_Abort[where 'a="'a :: comm_ring_1 fps", code]
 
-lemma open_fps_def: "open (S :: 'a::comm_ring_1 fps set) = (\<forall>a \<in> S. \<exists>r. r >0 \<and> ball a r \<subseteq> S)"
-  unfolding open_dist ball_def subset_eq by simp
+lemma open_fps_def: "open (S :: 'a::comm_ring_1 fps set) = (\<forall>a \<in> S. \<exists>r. r >0 \<and> {y. dist y a < r} \<subseteq> S)"
+  unfolding open_dist subset_eq by simp
 
 text \<open>The infinite sums and justification of the notation in textbooks.\<close>