src/HOL/Library/Bourbaki_Witt_Fixpoint.thy
changeset 63562 6f7a9d48a828
parent 63561 fba08009ff3e
child 64267 b9a1486e79be
     1.1 --- a/src/HOL/Library/Bourbaki_Witt_Fixpoint.thy	Fri Jul 29 09:49:23 2016 +0200
     1.2 +++ b/src/HOL/Library/Bourbaki_Witt_Fixpoint.thy	Fri Jul 29 11:42:13 2016 +0200
     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: -- \<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"