src/HOL/Library/Bourbaki_Witt_Fixpoint.thy

 lemma funpow_in_Chains: "{(f ^^ k) a |k. True} \<in> Chains leq"
 using chain_iterates_above[OF a] fun_pow_iterates_above
 by (blast intro: ChainsI dest: in_ChainsD)
 
 lemma fixp_above_Kleene_iter:
-  assumes "\<forall>M \<in> Chains leq. finite M" (* convenient but surely not necessary *)
+  assumes "\<forall>M \<in> Chains leq. finite M"  \<comment> \<open>convenient but surely not necessary\<close>
   assumes "(f ^^ Suc k) a = (f ^^ k) a"
   shows "fixp_above a = (f ^^ k) a"
 proof(rule leq_antisym)
   show "(fixp_above a, (f ^^ k) a) \<in> leq" using assms a
     by(auto simp add: fixp_above_def chain_iterates_above Chain_finite_iterates_above_fun_pow_iff funpow_stability[OF assms(2)] intro!: lub_least intro: iterates_above.base)