src/HOL/Library/Bourbaki_Witt_Fixpoint.thy
changeset 64911 f0e07600de47
parent 64267 b9a1486e79be
child 67408 4a4c14b24800
     1.1 --- a/src/HOL/Library/Bourbaki_Witt_Fixpoint.thy	Tue Jan 17 11:26:21 2017 +0100
     1.2 +++ b/src/HOL/Library/Bourbaki_Witt_Fixpoint.thy	Tue Jan 17 13:59:10 2017 +0100
     1.3 @@ -268,7 +268,7 @@
     1.4  
     1.5  context bourbaki_witt_fixpoint begin
     1.6  
     1.7 -lemma in_Chains_finite: -- \<open>Translation from @{thm in_chain_finite}.\<close>
     1.8 +lemma in_Chains_finite: \<comment> \<open>Translation from @{thm in_chain_finite}.\<close>
     1.9    assumes "M \<in> Chains leq"
    1.10    and "M \<noteq> {}"
    1.11    and "finite M"