# HG changeset patch
# User eberlm <eberlm@in.tum.de>
# Date 1501760128 -7200
# Node ID 56f8bfe1211cdac8f0be259b6247a277fcb00ded
# Parent  9a4c049f899735e5aee85948dce71558bf994fbe
Removed unnecessary constant 'ball' from Formal_Power_Series

diff -r 9a4c049f8997 -r 56f8bfe1211c src/HOL/Computational_Algebra/Formal_Power_Series.thy
--- a/src/HOL/Computational_Algebra/Formal_Power_Series.thy	Thu Aug 03 11:38:55 2017 +0200
+++ b/src/HOL/Computational_Algebra/Formal_Power_Series.thy	Thu Aug 03 13:35:28 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>