--- a/src/HOL/Library/Countable_Set.thy Tue Feb 13 14:24:50 2018 +0100
+++ b/src/HOL/Library/Countable_Set.thy Thu Feb 15 12:11:00 2018 +0100
@@ -266,7 +266,7 @@
by(induction n)(simp_all add: assms)
lemma countable_rtrancl:
- "(\<And>Y. countable Y \<Longrightarrow> countable (X `` Y)) \<Longrightarrow> countable Y \<Longrightarrow> countable (X^* `` Y)"
+ "(\<And>Y. countable Y \<Longrightarrow> countable (X `` Y)) \<Longrightarrow> countable Y \<Longrightarrow> countable (X\<^sup>* `` Y)"
unfolding rtrancl_is_UN_relpow UN_Image by (intro countable_UN countableI_type countable_relpow)
lemma countable_lists[intro, simp]: