diff -r 279da0358aa9 -r 09a6c44a48ea doc-src/TutorialI/Advanced/simp.thy --- 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]"}