src/HOL/Library/Bourbaki_Witt_Fixpoint.thy
changeset 67408 4a4c14b24800
parent 64911 f0e07600de47
     1.1 --- a/src/HOL/Library/Bourbaki_Witt_Fixpoint.thy	Fri Jan 12 14:43:06 2018 +0100
     1.2 +++ b/src/HOL/Library/Bourbaki_Witt_Fixpoint.thy	Fri Jan 12 15:27:46 2018 +0100
     1.3 @@ -357,7 +357,7 @@
     1.4  by (blast intro: ChainsI dest: in_ChainsD)
     1.5  
     1.6  lemma fixp_above_Kleene_iter:
     1.7 -  assumes "\<forall>M \<in> Chains leq. finite M" (* convenient but surely not necessary *)
     1.8 +  assumes "\<forall>M \<in> Chains leq. finite M"  \<comment> \<open>convenient but surely not necessary\<close>
     1.9    assumes "(f ^^ Suc k) a = (f ^^ k) a"
    1.10    shows "fixp_above a = (f ^^ k) a"
    1.11  proof(rule leq_antisym)