--- 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