diff -r fa5476c54731 -r 56247fdb8bbb src/Doc/Tutorial/ToyList/ToyList.thy --- a/src/Doc/Tutorial/ToyList/ToyList.thy Mon Dec 06 15:10:15 2021 +0100 +++ b/src/Doc/Tutorial/ToyList/ToyList.thy Mon Dec 06 15:34:54 2021 +0100 @@ -107,7 +107,7 @@ When Isabelle prints a syntax error message, it refers to the HOL syntax as the \textbf{inner syntax} and the enclosing theory language as the \textbf{outer syntax}. -Comments\index{comment} must be in enclosed in \texttt{(* }and\texttt{ *)}. +Comments\index{comment} must be in enclosed in \texttt{(*}and\texttt{*)}. \section{Evaluation} \index{evaluation}