Resolved codegen problem with uniformity for formal Laurent series
authorManuel Eberl <eberlm@in.tum.de>
Mon, 04 Feb 2019 19:05:52 +0100
changeset 69792 d21789843f01
parent 69791 195aeee8b30a
child 69793 0f2dc49250fb
Resolved codegen problem with uniformity for formal Laurent series
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