diff -r f321d21b9a6b -r aed0a0450797 doc-src/TutorialI/Inductive/advanced-examples.tex --- a/doc-src/TutorialI/Inductive/advanced-examples.tex Fri Jan 12 18:00:12 2001 +0100 +++ b/doc-src/TutorialI/Inductive/advanced-examples.tex Fri Jan 12 18:00:40 2001 +0100 @@ -28,7 +28,8 @@ over sets. It returns the set of ground terms that can be formed over a set \isa{F} of function symbols. For example, we could consider the set of ground terms formed from the finite -set {\isa{\{Number 2, UnaryMinus, Plus\}}}. +set \isa{\isacharbraceleft Number 2, UnaryMinus, +Plus\isacharbraceright}. This concept is inductive. If we have a list \isa{args} of ground terms over~\isa{F} and a function symbol \isa{f} in \isa{F}, then we