--- a/doc-src/TutorialI/Advanced/simp.thy Thu Jul 26 18:23:38 2001 +0200
+++ b/doc-src/TutorialI/Advanced/simp.thy Fri Aug 03 18:04:55 2001 +0200
@@ -45,7 +45,7 @@
congruence rule for @{text if}. Analogous rules control the evaluation of
@{text case} expressions.
-You can declare your own congruence rules with the attribute @{text cong},
+You can declare your own congruence rules with the attribute \attrdx{cong},
either globally, in the usual manner,
\begin{quote}
\isacommand{declare} \textit{theorem-name} @{text"[cong]"}