src/Doc/Tutorial/ToyList/ToyList.thy
changeset 74887 56247fdb8bbb
parent 69597 ff784d5a5bfb
child 80914 d97fdabd9e2b
--- 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}