diff -r 4b47d8aaf5af -r 5eebea8f359f doc-src/TutorialI/Inductive/advanced-examples.tex
--- a/doc-src/TutorialI/Inductive/advanced-examples.tex	Thu Jan 25 11:59:52 2001 +0100
+++ b/doc-src/TutorialI/Inductive/advanced-examples.tex	Thu Jan 25 15:31:31 2001 +0100
@@ -137,7 +137,7 @@
 Applying this as an elimination rule yields one case where \isa{even.cases}
 would yield two.  Rule inversion works well when the conclusions of the
 introduction rules involve datatype constructors like \isa{Suc} and \isa{\#}
-(list `cons'); freeness reasoning discards all but one or two cases.
+(list ``cons''); freeness reasoning discards all but one or two cases.
 
 In the \isacommand{inductive\_cases} command we supplied an
 attribute, \isa{elim!}, indicating that this elimination rule can be applied