# HG changeset patch
# User nipkow
# Date 1107759734 -3600
# Node ID 9d012c7fadab5eb2166b0e73ef22a49658f5b2cc
# Parent  59ebd778718c268f9132c3ced773befadcfbe835
fixed latex problems

diff -r 59ebd778718c -r 9d012c7fadab src/HOL/Finite_Set.thy
--- a/src/HOL/Finite_Set.thy	Sun Feb 06 13:12:32 2005 +0100
+++ b/src/HOL/Finite_Set.thy	Mon Feb 07 08:02:14 2005 +0100
@@ -1997,7 +1997,7 @@
 qed
 
 
-subsubsection{* Lemmas about {@text fold1} *}
+subsubsection{* Lemmas about @{text fold1} *}
 
 lemma (in ACf) fold1_Un:
 assumes A: "finite A" "A \<noteq> {}"