src/HOL/Finite_Set.thy

--- a/src/HOL/Finite_Set.thy	Sat Apr 10 20:22:07 2021 +0200
+++ b/src/HOL/Finite_Set.thy	Sun Apr 11 07:35:24 2021 +0000
@@ -2312,6 +2312,7 @@
   for S :: "'a::linordered_ring set"
   by (rule ccontr) (auto simp: abs_eq_iff vimage_def dest: inf_img_fin_dom)
 
+
 subsection \<open>The finite powerset operator\<close>
 
 definition Fpow :: "'a set \<Rightarrow> 'a set set"