src/HOL/Finite_Set.thy
changeset 15502 9d012c7fadab
parent 15500 dd4ab096f082
child 15504 5bc81e50f2c5
--- 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> {}"