# HG changeset patch
# User Andreas Lochbihler
# Date 1469785333 -7200
# Node ID 6f7a9d48a82879db8a431eea450132d02da6081d
# Parent  fba08009ff3efc45c46f8f16433940b24860232e
fix LaTeX error

diff -r fba08009ff3e -r 6f7a9d48a828 src/HOL/Library/Bourbaki_Witt_Fixpoint.thy
--- a/src/HOL/Library/Bourbaki_Witt_Fixpoint.thy	Fri Jul 29 09:49:23 2016 +0200
+++ b/src/HOL/Library/Bourbaki_Witt_Fixpoint.thy	Fri Jul 29 11:42:13 2016 +0200
@@ -268,7 +268,7 @@
 
 context bourbaki_witt_fixpoint begin
 
-lemma in_Chains_finite: -- \<open>Translation from @{thm in_chain_finite}. }\<close>
+lemma in_Chains_finite: -- \<open>Translation from @{thm in_chain_finite}.\<close>
   assumes "M \<in> Chains leq"
   and "M \<noteq> {}"
   and "finite M"