doc-src/TutorialI/Sets/sets.tex

 Here \isa{wf\ r} expresses that the relation~\isa{r} is well-founded.
 
 Many familiar induction principles are instances of this rule. 
 For example, the predecessor relation on the natural numbers 
 is well-founded; induction over it is mathematical induction. 
-The `tail of' relation on lists is well-founded; induction over 
+The ``tail of'' relation on lists is well-founded; induction over 
 it is structural induction. 
 
 Well-foundedness can be difficult to show. The various 
 formulations are all complicated.  However,  often a relation
 is well-founded by construction.  HOL provides