# HG changeset patch
# User Manuel Eberl <eberlm@in.tum.de>
# Date 1549303552 -3600
# Node ID d21789843f01bb6f6b73bc36de0881a62736234e
# Parent  195aeee8b30a329c753d1ef6888ea5a9956a54f3
Resolved codegen problem with uniformity for formal Laurent series

diff -r 195aeee8b30a -r d21789843f01 src/HOL/Computational_Algebra/Formal_Laurent_Series.thy
--- a/src/HOL/Computational_Algebra/Formal_Laurent_Series.thy	Mon Feb 04 17:19:04 2019 +0100
+++ b/src/HOL/Computational_Algebra/Formal_Laurent_Series.thy	Mon Feb 04 19:05:52 2019 +0100
@@ -4161,6 +4161,8 @@
 end
 end
 
+declare uniformity_Abort[where 'a="'a :: group_add fls", code]
+
 lemma open_fls_def:
   "open (S :: 'a::group_add fls set) = (\<forall>a \<in> S. \<exists>r. r >0 \<and> {y. dist y a < r} \<subseteq> S)"
   unfolding open_dist subset_eq by simp