# HG changeset patch
# User eberlm <eberlm@in.tum.de>
# Date 1502111437 -7200
# Node ID a8b89392ecb613f5551626cc72fde1d1c5e39b6b
# Parent  1f66c7d77002149f9f339136e03f2e9b1292562b# Parent  e2f426b54922f6506bab6ffe3ece47762d66866b
Merged

diff -r e2f426b54922 -r a8b89392ecb6 src/HOL/Computational_Algebra/Formal_Power_Series.thy
--- a/src/HOL/Computational_Algebra/Formal_Power_Series.thy	Mon Aug 07 14:40:35 2017 +0200
+++ b/src/HOL/Computational_Algebra/Formal_Power_Series.thy	Mon Aug 07 15:10:37 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>