doc-src/TutorialI/Misc/cond_rewr.thy

--- a/doc-src/TutorialI/Misc/cond_rewr.thy	Fri Aug 04 23:02:11 2000 +0200
+++ b/doc-src/TutorialI/Misc/cond_rewr.thy	Sun Aug 06 15:26:53 2000 +0200
@@ -13,8 +13,7 @@
 text{*\noindent
 Note the use of ``\ttindexboldpos{,}{$Isar}'' to string together a
 sequence of methods. Assuming that the simplification rule
-*}(*<*)term(*>*) "(rev xs = []) = (xs = [])";
-text{*\noindent
+@{term"(rev xs = []) = (xs = [])"}
 is present as well,
 *}